Theorems · Definition · linear algebra

Submodule.IsPrincipal.casesOn

{R : Type u_1} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {S : Submodule R M} →
            {motive : S.IsPrincipal → Sort u} →
              (t : S.IsPrincipal) → ((principal : ∃ a, S = R ∙ a) → motive ⋯) → motive t

Defined in: Mathlib.LinearAlgebra.Span.Defs
Cited by: 15 results in Mathlib
Foundations: Depth 20 from the axioms · uses propext, Quot.sound
Assumes: Semiring AddCommMonoid Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Modulestatement and proof · cited by 20,661
Semiringstatement and proof · cited by 13,802
AddCommMonoidstatement and proof · cited by 12,281
Submodulestatement and proof · cited by 7,192
Submodule.spanstatement and proof · cited by 1,504
Submodule.IsPrincipalstatement and proof · cited by 129

Cited by15

Results whose statement or proof uses this declaration.

Int.ideal_span_absNorm_eq_selfproof · cited by 4
PrincipalIdealRing.isMaximal_of_irreducibleproof · cited by 4
Ideal.isPrincipal_of_isPrincipal_isLocalizationAway_of_primeproof · cited by 2
Submodule.isPrincipal_iffproof · cited by 2
IsLocalization.coeSubmodule_isPrincipalproof · cited by 2
Valuation.Integers.isPrincipal_iff_exists_isGreatestproof · cited by 2
exists_maximalIdeal_pow_eq_of_principalproof · cited by 1
RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Iccproof · cited by 1
IsBezout.iff_span_pair_isPrincipalproof · cited by 1
Ideal.exists_normalized_span_of_isPrincipalproof · cited by 1
Module.Baer.of_divisibleproof · cited by 1
Ideal.exists_mem_span_singleton_map_residueField_eqproof · cited by 0