toIntAlgHom_coe — Mathlib

English

Let R and S be rings and f: R →+* S a ring hom. The associated integer-algebra hom f.toIntAlgHom has the same action as f; i.e., it is the same map when viewed as a function.

Русский

Пусть R и S — кольца и f: R →+* S — кольцевой гомоморфизм. Соответствующий интегрально-алгебраический гомоморфизм f.toIntAlgHom действует так же, как и f; то есть это та же самая функция.

LaTeX

$$$ \\forall x\\,\\, (f^{\\mathrm{IntAlg}})(x) = f(x) $$$

Lean4

@[simp]
theorem toIntAlgHom_coe [Ring R] [Ring S] (f : R →+* S) : ⇑f.toIntAlgHom = ⇑f :=
  rfl

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