Theorems · Inductive type · linear algebra
Submodule.IsPrincipal
{R : Type u_1} →
{M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → PropAn R-submodule of M is principal if it is generated by one element.
- Defined in
- Mathlib.LinearAlgebra.Span.Defs
- Cited by
- 129 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 5 definitions · uses no axioms
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement · cited by 20,661
- Semiringstatement · cited by 13,802
- AddCommMonoidstatement · cited by 12,281
- Submodulestatement · cited by 7,192
Cited by151
Results whose statement or proof uses this declaration.
- Submodule.IsPrincipal.generatorstatement and proof · cited by 56
- Ideal.span_singleton_generatorstatement and proof · cited by 17
- Submodule.IsPrincipal.casesOnstatement and proof · cited by 15
- IsBezout.gcdstatement and proof · cited by 12
- Submodule.IsPrincipal.mem_iff_generator_dvdstatement and proof · cited by 11
- Submodule.IsPrincipal.principalstatement and proof · cited by 10
- Submodule.IsPrincipal.span_singleton_generatorstatement and proof · cited by 10
- Submodule.IsPrincipal.generator_memstatement and proof · cited by 9
- Ideal.associatesEquivIsPrincipalstatement and proof · cited by 9
- Submodule.IsPrincipal.eq_bot_iff_generator_eq_zerostatement and proof · cited by 7
- IsBezout.span_gcdstatement and proof · cited by 5
- Ideal.associatesNonZeroDivisorsEquivIsPrincipalstatement and proof · cited by 5