Structures · Algebra
IsLocalRing
A semiring is local if it is nontrivial and a or b is a unit whenever a + b = 1.
Note that IsLocalRing is a predicate.
- Defined in
- Mathlib.RingTheory.LocalRing.Defs
- Shape
- One type argument · adds isUnit_or_isUnit_of_add_one
Extends1
Extended by3
Concrete types that are instances10
- Nat
- CommRingCat.carrier
- TensorProduct
- PadicInt
- Localization
- MvPowerSeries
- AdicCompletion
- DualNumber
- HomogeneousLocalization.AtPrime
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by378
- IsLocalRing.maximalIdeal
- IsLocalRing.ResidueField
- IsLocalRing.residue
- IsLocalRing.closedPoint
- IsLocalRing.le_maximalIdeal
- IsLocalRing.eq_maximalIdeal
- AlgebraicGeometry.Scheme.stalkClosedPointTo
- IsLocalRing.ResidueField.map
- IsLocalRing.maximalIdeal_le_jacobson
- IsLocalRing.CotangentSpace
- PowerSeries.IsWeierstrassFactorization
- PowerSeries.IsWeierstrassDivisor.of_map_ne_zero
- PowerSeries.weierstrassMod
- IsLocalRing.residue_surjective
- IsLocalRing.jacobson_eq_maximalIdeal
- PowerSeries.IsWeierstrassDivision
- IsLocalRing.local_hom_TFAE
- PowerSeries.weierstrassDiv
- AlgebraicGeometry.stalkClosedPointIso
- PowerSeries.weierstrassDistinguished
- IsLocalization.AtPrime.map_eq_maximalIdeal
- PowerSeries.weierstrassUnit
- IsLocalRing.isField_iff_maximalIdeal_eq
- IsLocalization.AtPrime.equivQuotMaximalIdeal
- Module.free_of_flat_of_isLocalRing
- IsLocalRing.mem_maximalIdeal
- RingHom.domain_isLocalRing
- IsLocalRing.specializes_closedPoint
- PowerSeries.IsWeierstrassFactorization.elim
- IsLocalRing.ResidueField.mapEquiv
- PowerSeries.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
- IsLocalRing.isUnit_or_isUnit_of_add_one
- Algebra.FormallyUnramified.map_maximalIdeal
- IsLocalHom.of_surjective
- isRegularLocalRing_iff
- AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem
- AlgebraicGeometry.Scheme.germ_stalkClosedPointTo
- IsLocalRing.subsingleton_tensorProduct
- IsLocalRing.map_tensorProduct_mk_eq_top
- IsLocalRing.comap_closedPoint
- IsLocalRing.residue_eq_zero_iff
- IsDedekindDomain.primesOverEquivPrimesOver
- AdicCompletion.isLocalRing_of_fg
- IsLocalRing.ringJacobson_eq_maximalIdeal
- IsLocalRing.isUnit_or_isUnit_of_isUnit_add
- IsLocalRing.maximalIdeal_height_eq_ringKrullDim
- PowerSeries.exists_isWeierstrassFactorization
- IsLocalRing.basisQuotient
- IsLocalRing.notMem_maximalIdeal
- LocalSubring.range