castHom_self — Mathlib

English

The castHom map from ZMod n into RingHom (ZMod n) is identical to the identity ring hom; i.e., castHom dvd_rfl (ZMod n) = RingHom.id (ZMod n).

Русский

Гомоморфизм castHom от ZMod n в RingHom (ZMod n) совпадает с тождественным гомоморфизмом; то есть castHom = id.

LaTeX

$$$\text{castHom }\ dvd\_rfl\; (\mathbb{Z}/n\mathbb{Z}) = \mathrm{RingHom}.id(\mathbb{Z}/n\mathbb{Z})$$$

Lean4

@[simp]
theorem castHom_self : ZMod.castHom dvd_rfl (ZMod n) = RingHom.id (ZMod n) :=
  Subsingleton.elim _ _

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