NonLocalRing

📁 Source: Mathlib/RingTheory/LocalRing/NonLocalRing.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_surjective_of_not_isLocalRing, not_isLocalRing_def, not_isLocalRing_of_nontrivial_pi, not_isLocalRing_of_prod_of_nontrivial, not_isLocalRing_tfae	5
Total	5

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_surjective_of_not_isLocalRing 📖	mathematical	IsLocalRing CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe RingHom Semiring.toNonAssocSemiring Prod.instNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	—	List.TFAE.out not_isLocalRing_tfae Ideal.isCoprime_of_isMaximal Ideal.instIsTwoSided_1 RingEquiv.surjective Ideal.Quotient.mk_surjective
not_isLocalRing_def 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	IsLocalRing	—	isUnit_or_isUnit_of_add_one
not_isLocalRing_of_nontrivial_pi 📖	mathematical	Nontrivial	IsLocalRing Pi.semiring	—	exists_pair_ne not_isUnit_zero NeZero.one IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass not_isLocalRing_def add_zero zero_add
not_isLocalRing_of_prod_of_nontrivial 📖	mathematical	—	IsLocalRing Prod.instSemiring	—	not_isUnit_zero NeZero.one IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass not_isLocalRing_def add_zero zero_add
not_isLocalRing_tfae 📖	mathematical	—	List.TFAE IsLocalRing CommSemiring.toSemiring Nontrivial MaximalSpectrum Ideal Ideal.IsMaximal	—	not_subsingleton_iff_nontrivial of_singleton_maximalSpectrum MaximalSpectrum.instNonemptyOfNontrivial eq_maximalIdeal List.tfae_of_cycle

---

← Back to Index