map_smul_of_tower — Mathlib

English

If φ: A →ₗc[R] B is a coalgebra homomorphism and A,B have an additional scalar action of R' compatible with R, then φ(r·x) = r·φ(x) for all r ∈ R', x ∈ A.

Русский

Если φ: A →ₗc[R] B — коалгоморфизм, и на A,B задано дополнительное действие скаляра R', совместимое с R, то φ(r·x) = r·φ(x) для всех r ∈ R', x ∈ A.

LaTeX

$$$\varphi(r \cdot x) = r \cdot \varphi(x)$$$

Lean4

theorem map_smul_of_tower {R'} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul A B R' R] (r : R') (x : A) :
    φ (r • x) = r • φ x :=
  φ.toLinearMap.map_smul_of_tower r x

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