smul_toAlgebra — Mathlib

English

For a ring hom i: R →+* S, and elements r∈R, s∈S, the scalar action by r matches i(r) acting on s in the Algebra' construction.

Русский

Для гомоморфизма i: R →+* S и элементов r∈R, s∈S, действие скаляра r соответствует i(r) действует на s в конструкции Algebra'.

LaTeX

$$$r \cdot s = i(r) \cdot s$.$$

Lean4

theorem smul_toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) (r : R) (s : S) :
    let _ := RingHom.toAlgebra i
    r • s = i r * s :=
  rfl

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