residueField — Mathlib

English

The residue field of ℤ_p is canonically isomorphic to Z/pZ; this is formalized via a residue field equivalence.

Русский

Поле остатка ℤ_p канонически изоморфно Z/pZ; реализовано через эквивалентность остаточного поля.

LaTeX

$$IsLocalRing.ResidueField(ℤ_p) ≃+* ZMod(p)$$

Lean4

/-- The equivalence between the residue field of the `p`-adic integers and `ℤ/pℤ` -/
def residueField : IsLocalRing.ResidueField ℤ_[p] ≃+* ZMod p :=
  (Ideal.quotEquivOfEq PadicInt.ker_toZMod.symm).trans <|
    RingHom.quotientKerEquivOfSurjective (ZMod.ringHom_surjective PadicInt.toZMod)

Похожие утверждения