Pseudo-null modules, characteristic ideals, and height one localizations

theorem Module.charIdeal_eq_one_of_isPseudoNull (A : Type u_1) [CommRing A] (M : Type u_2) [AddCommGroup M] [Module A M] [IsPseudoNull A M] : charIdeal A M = 1

theorem LinearMap.IsPseudoIsomorphism.charIdeal_eq {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {N : Type u_3} [AddCommGroup N] [Module A N] {f : M →ₗ[A] N} (H : f.IsPseudoIsomorphism) : Module.charIdeal A M = Module.charIdeal A N

theorem Module.IsPseudoIsomorphic.charIdeal_eq {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {N : Type u_3} [AddCommGroup N] [Module A N] (H : M ∼ₚᵢₛ[A] N) : charIdeal A M = charIdeal A N