Basic

📁 Source: Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

Statistics

Metric	Count
Definitions instUniqueMaximalSpectrum	1
Theorems eq_maximalIdeal, isField_iff_maximalIdeal_eq, isMaximal_iff, jacobson_eq_maximalIdeal, ker_eq_maximalIdeal, le_maximalIdeal, le_maximalIdeal_of_isPrime, isMaximal, maximalIdeal_eq_bot, maximalIdeal_le_jacobson, maximal_ideal_unique, mem_maximalIdeal, notMem_maximalIdeal, of_singleton_maximalSpectrum, ringJacobson_eq_maximalIdeal, isLocalRing_of_unit, isLocalRing_of_unit	17
Total	18

IsLocalRing

Definitions

Name	Category	Theorems
instUniqueMaximalSpectrum 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_maximalIdeal 📖	mathematical	—	maximalIdeal	—	ExistsUnique.unique maximal_ideal_unique maximalIdeal.isMaximal
isField_iff_maximalIdeal_eq 📖	mathematical	—	IsField CommSemiring.toSemiring maximalIdeal Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	not_iff_not Ring.ne_bot_of_isMaximal_of_not_isField toNontrivial maximalIdeal.isMaximal Ring.not_isField_iff_exists_prime Ideal.IsMaximal.isPrime'
isMaximal_iff 📖	mathematical	—	Ideal.IsMaximal CommSemiring.toSemiring maximalIdeal	—	Ideal.IsMaximal.eq_of_le Ideal.IsMaximal.out maximalIdeal.isMaximal Ideal.eq_top_of_isUnit_mem
jacobson_eq_maximalIdeal 📖	mathematical	—	Ideal.jacobson CommRing.toRing maximalIdeal CommRing.toCommSemiring	—	le_antisymm sInf_le le_maximalIdeal maximalIdeal.isMaximal maximalIdeal_le_jacobson
ker_eq_maximalIdeal 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.instFunLike	RingHom.ker RingHom.instRingHomClass maximalIdeal	—	eq_maximalIdeal RingHom.instRingHomClass RingHom.ker_isMaximal_of_surjective
le_maximalIdeal 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule maximalIdeal	—	Ideal.exists_le_maximal eq_maximalIdeal
le_maximalIdeal_of_isPrime 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule maximalIdeal	—	le_maximalIdeal Ideal.IsPrime.ne_top
maximalIdeal_eq_bot 📖	mathematical	—	maximalIdeal Semifield.toCommSemiring Field.toSemifield Field.instIsLocalRing Bot.bot Ideal CommSemiring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Field.instIsLocalRing isField_iff_maximalIdeal_eq Field.toIsField
maximalIdeal_le_jacobson 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule maximalIdeal Ideal.jacobson CommRing.toRing	—	le_sInf le_of_eq eq_maximalIdeal
maximal_ideal_unique 📖	mathematical	—	ExistsUnique Ideal CommSemiring.toSemiring Ideal.IsMaximal	—	—
mem_maximalIdeal 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule maximalIdeal Set Set.instMembership nonunits MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
notMem_maximalIdeal 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule maximalIdeal IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
of_singleton_maximalSpectrum 📖	mathematical	—	IsLocalRing CommSemiring.toSemiring	—	of_unique_max_ideal MaximalSpectrum.isMaximal
ringJacobson_eq_maximalIdeal 📖	mathematical	—	Ring.jacobson CommRing.toRing maximalIdeal CommRing.toCommSemiring	—	Ideal.jacobson_bot jacobson_eq_maximalIdeal top_ne_bot Ideal.instNontrivial toNontrivial

IsLocalRing.maximalIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMaximal 📖	mathematical	—	Ideal.IsMaximal CommSemiring.toSemiring IsLocalRing.maximalIdeal	—	Ideal.isMaximal_iff isUnit_one mem_nonunits_iff IsLocalRing.mem_maximalIdeal Units.inv_mul Ideal.mul_mem_left

Subring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalRing_of_unit 📖	mathematical	IsUnit Subring SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring toRing	IsLocalRing	—	Subsemiring.isLocalRing_of_unit

Subsemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalRing_of_unit 📖	mathematical	IsUnit Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero toSemiring	IsLocalRing	—	nontrivial IsLocalRing.toNontrivial IsLocalRing.isUnit_or_isUnit_of_add_one Subtype.prop

---

← Back to Index