smul_toAlgebra' — Mathlib

English

The smul action of R on S in the Algebra' construction coincides with multiplication by i(r) on S.

Русский

Действие умножения на R на S в конструкциях Algebra' совпадает с умножением на i(r) в S.

LaTeX

$$$r \cdot s = i(r) \cdot s$ for all $r\in R$, $s\in S$ in the constructed Algebra'.$$

Lean4

theorem smul_toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ c x, i c * x = x * i c) (r : R)
    (s : S) :
    let _ := RingHom.toAlgebra' i h
    r • s = i r * s :=
  rfl

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