toRatAlgHom_apply — Mathlib

English

Let R and S be rings with ℚ-algebra structures, and let f be a ring homomorphism from R to S. The induced ℚ-algebra homomorphism f̃ agrees with f on every element of R; i.e., f̃(x) = f(x) for all x ∈ R.

Русский

Пусть R и S — кольца, над которыми задана структура ℚ-алгебр, и пусть f: R → S — кольтовый гомоморфизм. Индуцированный ℚ-алгебра-гомоморфизм f̃ действует на любой x ∈ R так же, как f: f̃(x) = f(x).

LaTeX

$$$\\forall x \\in R,\\ f^{\\mathbb{Q}}(x) = f(x)$$$

Lean4

@[simp]
theorem toRatAlgHom_apply [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) (x : R) : f.toRatAlgHom x = f x :=
  rfl

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