map_id — Mathlib

English

Applying IsLocalRing.ResidueField.map to the identity ring homomorphism yields the identity ring homomorphism.

Русский

Применение IsLocalRing.ResidueField.map к тождественному кольцевому гомоморфизму дает тождественный кольцевой гомоморфизм.

LaTeX

$$$\\mathrm{IsLocalRing.ResidueField.map} (\\mathrm{RingHom.id} \\; R) = \\mathrm{RingHom.id} (\\mathrm{IsLocalRing.ResidueField} R)$$$

Lean4

/-- Applying `IsLocalRing.ResidueField.map` to the identity ring homomorphism gives the identity
ring homomorphism. -/
@[simp]
theorem map_id : IsLocalRing.ResidueField.map (RingHom.id R) = RingHom.id (IsLocalRing.ResidueField R) :=
  Ideal.Quotient.ringHom_ext <| RingHom.ext fun _ => rfl

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