IsPrimary

📁 Source: Mathlib/RingTheory/IsPrimary.lean

Statistics

Metric	Count
Definitions IsPrimary	1
Theorems inf, isPrime_radical_colon, mem_or_mem, ne_top, radical_colon_singleton_of_notMem, isPrimary_finsetInf, isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul	7
Total	8

Submodule

Definitions

Name	Category	Theorems
IsPrimary 📖	MathDef	3 math math: IsMinimalPrimaryDecomposition.primary, isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul, InfIrred.isPrimary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrimary_finsetInf 📖	mathematical	Finset Finset.instMembership IsPrimary Ideal.radical colon CommSemiring.toSemiring Set.univ	Finset.inf Submodule Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instOrderTop	—	Finset.induction_on Finset.eq_empty_or_nonempty Finset.instLawfulSingleton Finset.inf_singleton Finset.inf_insert Finset.mem_insert_of_mem IsPrimary.inf colon_finsetInf Ideal.radical_finset_inf Finset.mem_insert_self
isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul 📖	mathematical	—	IsPrimary CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule HasQuotient.Quotient CommSemiring.toSemiring hasQuotient CommRing.toRing Quotient.addCommGroup Quotient.module SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Quotient.distribMulAction Quotient.smulCommClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SemigroupAction.toSMul Monoid.toSemigroup Ring.toSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid CommMonoid.toMonoid Monoid.toNatPow Top.top instTop Bot.bot instBot	—	Quotient.smulCommClass smulCommClass_self Function.Surjective.forall mkQ_surjective SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass ker_mkQ RingHomSurjective.ids LinearMap.range_eq_top map_top

Submodule.IsPrimary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf 📖	mathematical	Submodule.IsPrimary Ideal.radical Submodule.colon CommSemiring.toSemiring Set.univ	Submodule Submodule.instMin	—	smulCommClass_self Submodule.inf_colon Ideal.radical_inf inf_idem
isPrime_radical_colon 📖	mathematical	Submodule.IsPrimary	Ideal.IsPrime CommSemiring.toSemiring Ideal.radical Submodule.colon Set.univ	—	Ideal.isPrime_iff smulCommClass_self mul_pow SemigroupAction.mul_smul Ideal.mem_radical_of_pow_mem
mem_or_mem 📖	mathematical	Submodule.IsPrimary Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Ideal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.radical Submodule.colon Top.top Set BooleanAlgebra.toTop Set.instBooleanAlgebra	—	—
ne_top 📖	—	Submodule.IsPrimary	—	—	—
radical_colon_singleton_of_notMem 📖	mathematical	Submodule.IsPrimary Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike	Ideal.radical Submodule.colon Set Set.instSingletonSet Set.univ	—	le_antisymm Ideal.radical_le_radical_iff Submodule.mem_colon_singleton Ideal.radical_mono Submodule.colon_mono le_rfl Set.subset_univ

---

← Back to Index