Defs

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

Statistics

Metric	Count
Definitions IsLocalRing	1
Theorems isUnit_or_isUnit_of_add_one, toNontrivial	2
Total	3

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_or_isUnit_of_add_one 📖	mathematical	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
toNontrivial 📖	mathematical	—	Nontrivial	—	—

(root)

Definitions

Name	Category	Theorems
IsLocalRing 📖	CompData	44 math math: LocalSubring.isLocalRing, ValuationRing.isLocalRing, ValuationRing.TFAE, instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap, smoothSheafCommRing.instLocalRing_stalk, isLocalRing_top, Localization.AtPrime.isLocalRing, IsLocalRing.of_surjective, PadicInt.instIsLocalRing, Ring.krullDimLE_zero_and_isLocalRing_tfae, IsLocalRing.of_unique_nonzero_prime, HenselianLocalRing.toIsLocalRing, ValuationSubring.isLocalRing, IsLocalRing.not_isLocalRing_def, IsLocalRing.of_unique_max_ideal, Field.instIsLocalRing, MvPowerSeries.instIsLocalRing, RingHom.domain_isLocalRing, IsLocalRing.of_subring', IsLocalRing.of_nonunits_add, instIsLocalRingNat, IsLocalRing.of_isMaximal_nilradical, IsDiscreteValuationRing.toIsLocalRing, IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add, Subring.isLocalRing_of_unit, ValuationRing.iff_local_bezout_domain, IsLocalRing.not_isLocalRing_of_prod_of_nontrivial, IsLocalRing.of_subring, IsLocalRing.not_isLocalRing_tfae, AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf, isLocalRing_of_isAdicComplete_maximal, IsLocalization.AtPrime.isLocalRing, RingEquiv.isLocalRing, HomogeneousLocalization.isLocalRing, DualNumber.instIsLocalRing, AlgebraicGeometry.LocallyRingedSpace.isLocalRing, IsLocalRing.of_injective, instIsLocalRingSubtypeMemSubringMapOfNontrivial, PowerSeries.instIsLocalRing, IsLocalRing.of_singleton_maximalSpectrum, IsLocalRing.not_isLocalRing_of_nontrivial_pi, IsLocalRing.of_surjective', IsLocalRing.of_isUnit_or_isUnit_one_sub_self, Subsemiring.isLocalRing_of_unit

---

← Back to Index