IsPrimary

📁 Source: Mathlib/RingTheory/Ideal/IsPrimary.lean

Statistics

Metric	Count
Definitions IsPrimary	1
Theorems comap, inf, isPrimary, isPrimary_finsetInf, isPrimary_finset_inf, isPrimary_iff, isPrimary_of_isMaximal_radical, isPrime_radical	8
Total	9

Ideal

Definitions

Name	Category	Theorems
IsPrimary 📖	MathDef	3 math math: IsPrime.isPrimary, isPrimary_iff, isPrimary_of_isMaximal_radical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrimary_finsetInf 📖	mathematical	Finset Finset.instMembership IsPrimary radical	Finset.inf Ideal CommSemiring.toSemiring Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instOrderTop	—	Submodule.isPrimary_finsetInf Submodule.colon_univ instIsTwoSided
isPrimary_finset_inf 📖	mathematical	Finset Finset.instMembership IsPrimary radical	Finset.inf Ideal CommSemiring.toSemiring Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instOrderTop	—	isPrimary_finsetInf
isPrimary_iff 📖	mathematical	—	IsPrimary Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule radical	—	IsPrimary.eq_1 Submodule.IsPrimary.eq_1 mul_comm smulCommClass_self IsScalarTower.left mul_top instIsTwoSided
isPrimary_of_isMaximal_radical 📖	mathematical	—	IsPrimary	—	isPrimary_iff IsMaximal.ne_top radical_top span_singleton_le_iff_mem IsScalarTower.left mul_top instIsTwoSided mul_add Distrib.leftDistribClass span_singleton_mul_span_singleton add_le_iff mul_le_left exists_le_maximal IsPrime.radical_le_iff IsMaximal.isPrime IsMaximal.eq_of_le
isPrime_radical 📖	mathematical	IsPrimary	IsPrime CommSemiring.toSemiring radical	—	Submodule.IsPrimary.isPrime_radical_colon Submodule.colon_univ instIsTwoSided

Ideal.IsPrimary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	Ideal.IsPrimary	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass	—	RingHom.instRingHomClass Ideal.isPrimary_iff Ideal.comap_ne_top map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
inf 📖	mathematical	Ideal.IsPrimary Ideal.radical	Ideal CommSemiring.toSemiring Submodule.instMin NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Submodule.IsPrimary.inf Submodule.colon_univ Ideal.instIsTwoSided

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrimary 📖	mathematical	—	Ideal.IsPrimary	—	Ideal.isPrimary_iff ne_top' Ideal.le_radical mem_or_mem

---

← Back to Index