map_smul_of_tower — Mathlib

English

Let f be an R-algebra homomorphism between S-algebras compatible with the R-tower. Then f is R-linear: for every c in R and every x in A, f(c · x) = c · f(x).

Русский

Пусть f является гомоморфизмом R-алгебр между S-алгебрами, совместимым с конструкцией-трансформацией по р-основанию. Тогда f линейна по R: для каждого c в R и каждого x в A выполняется f(c · x) = c · f(x).

LaTeX

$$$f(c \\cdot x) = c \\cdot f(x) \\quad (c \\in R, x \\in A).$$$

Lean4

theorem map_smul_of_tower {R S : Type*} [CommSemiring S] [SMul R A] [Algebra S A] [SMul R B] [Algebra S B]
    [MulActionHomClass (A →A[S] B) R A B] (f : A →A[S] B) (c : R) (x : A) : f (c • x) = c • f x :=
  map_smul f c x

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