Theorems · Theorem · commutative algebra

Module.exists_ker_toSpanSingleton_eq_annihilator

∀ (R : Type u) [inst : CommRing R] [IsPrincipalIdealRing R] (M : Type v) [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] [Module.Finite R M], ∃ x, (LinearMap.toSpanSingleton R M x).ker = Module.annihilator R M

Defined in

Mathlib.Algebra.Module.PID

Cited by

0 results in Mathlib

Foundations

Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsPrincipalIdealRingAddCommGroupModuleIsDomainModule.Finite