Defs

📁 Source: Mathlib/RingTheory/RegularLocalRing/Defs.lean

Statistics

Metric	Count
Definitions IsRegularLocalRing	1
Theorems iff_finrank_cotangentSpace, instOfIsLocalRingOfIsDomainOfIsPrincipalIdealRing, of_ringEquiv, of_spanFinrank_maximalIdeal_le, spanFinrank_maximalIdeal, toIsLocalRing, toIsNoetherian, isRegularLocalRing_iff	8
Total	9

IsRegularLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_finrank_cotangentSpace 📖	mathematical	—	IsRegularLocalRing WithBot ENat WithBot.natCast ENat.instNatCast Module.finrank IsLocalRing.ResidueField IsLocalRing.CotangentSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent IsLocalRing.maximalIdeal CommRing.toCommSemiring IsLocalRing.instModuleResidueFieldCotangentSpace ringKrullDim	—	isRegularLocalRing_iff IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace
instOfIsLocalRingOfIsDomainOfIsPrincipalIdealRing 📖	mathematical	—	IsRegularLocalRing	—	instIsNoetherianRingOfIsArtinianRing instIsArtinianOfIsSemisimpleModuleOfFinite IsSemisimpleRing.isSemisimpleModule instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule FiniteDimensional.finiteDimensional_self IsLocalRing.maximalIdeal_eq_bot Submodule.spanFinrank_bot CharP.cast_eq_zero CharP.ofCharZero WithBot.charZero ringKrullDim_eq_zero_of_field of_spanFinrank_maximalIdeal_le isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing Module.Finite.self IsPrincipalIdealRing.principal IsPrincipalIdealRing.ringKrullDim_eq_one WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid WithBot.zeroLEOneClass Set.ncard_singleton Submodule.spanFinrank_span_le_ncard_of_finite Set.finite_singleton
of_ringEquiv 📖	mathematical	—	IsRegularLocalRing	—	RingEquiv.isLocalRing toIsLocalRing isNoetherianRing_of_ringEquiv toIsNoetherian isRegularLocalRing_iff ringKrullDim_eq_of_ringEquiv IsLocalRing.map_ringEquiv_maximalIdeal Ideal.spanFinrank_map_eq_of_ringEquiv
of_spanFinrank_maximalIdeal_le 📖	mathematical	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.natCast ENat.instNatCast Submodule.spanFinrank CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal ringKrullDim	IsRegularLocalRing	—	isRegularLocalRing_iff le_antisymm ringKrullDim_le_spanFinrank_maximalIdeal
spanFinrank_maximalIdeal 📖	mathematical	—	WithBot ENat WithBot.natCast ENat.instNatCast Submodule.spanFinrank CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal toIsLocalRing ringKrullDim	—	—
toIsLocalRing 📖	mathematical	—	IsLocalRing CommSemiring.toSemiring CommRing.toCommSemiring	—	—
toIsNoetherian 📖	mathematical	—	IsNoetherian CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—

(root)

Definitions

Name	Category	Theorems
IsRegularLocalRing 📖	CompData	5 math math: IsRegularLocalRing.of_ringEquiv, isRegularLocalRing_iff, IsRegularLocalRing.of_spanFinrank_maximalIdeal_le, IsRegularLocalRing.instOfIsLocalRingOfIsDomainOfIsPrincipalIdealRing, IsRegularLocalRing.iff_finrank_cotangentSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRegularLocalRing_iff 📖	mathematical	—	IsRegularLocalRing WithBot ENat WithBot.natCast ENat.instNatCast Submodule.spanFinrank CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal ringKrullDim	—	—

---

← Back to Index