Theorems · Definition · commutative algebra
IsLocalRing.residue
(R : Type u_1) → [inst : CommRing R] → [inst_1 : IsLocalRing R] → R →+* IsLocalRing.ResidueField R
The quotient map from a local ring to its residue field.
- Cited by
- 71 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingIsLocalRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- RingHomstatement · cited by 10,189
- Ideal.Quotient.mkproof · cited by 610
- IsLocalRingstatement and proof · cited by 339
- IsLocalRing.maximalIdealproof · cited by 297
- IsLocalRing.ResidueFieldstatement · cited by 156
Cited by81
Results whose statement or proof uses this declaration.
- ArchimedeanClass.FiniteResidueField.mkproof · cited by 22
- AlgebraicGeometry.Scheme.residueproof · cited by 20
- PowerSeries.IsWeierstrassDivisor.of_map_ne_zerostatement and proof · cited by 11
- IsLocalRing.residue_surjectivestatement · cited by 11
- PowerSeries.weierstrassModproof · cited by 11
- PowerSeries.weierstrassDivproof · cited by 10
- PowerSeries.weierstrassDistinguishedstatement and proof · cited by 8
- PowerSeries.weierstrassUnitstatement and proof · cited by 8
- PowerSeries.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnitstatement and proof · cited by 5
- PowerSeries.IsWeierstrassFactorization.elimproof · cited by 5
- AlgebraicGeometry.LocallyRingedSpace.evaluation_naturalityproof · cited by 4
- IsLocalRing.residue_eq_zero_iffstatement · cited by 4