mapEquiv_refl — Mathlib

English

The residue-field functor sends the identity RingEquiv to the identity on the residue field.

Русский

Функтор поля остатка отправляет тождественную эквивалентность кольца в тождественный автоморфизм поля остатка.

LaTeX

$$$ \\operatorname{mapEquiv}(\\mathrm{RingEquiv}.refl\\, R) = \\mathrm{RingEquiv}.refl\\, (\\operatorname{IsLocalRing.ResidueField} R) $$$

Lean4

@[simp]
theorem mapEquiv_refl : mapEquiv (RingEquiv.refl R) = RingEquiv.refl _ :=
  RingEquiv.toRingHom_injective map_id

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