English
In a scalar tower A → B → C with IsScalarTower, the action of A on B and on C is compatible: the image of a • b in C equals a • (b viewed in C).
Русский
В пирамиде действия скаляров A → B → C с условием IsScalarTower действие A на B и на C согласованы: изображение a • b в C равно a • (образ B в C).
LaTeX
$$$((a \\cdot b) : C) = a \\cdot (b : C)$ \n\\text{(under IsScalarTower A B C)}$$
Lean4
@[norm_cast]
theorem coe_smul (A B C : Type*) [SMul A B] [CommSemiring B] [Semiring C] [Algebra B C] [SMul A C] [IsScalarTower A B C]
(a : A) (b : B) : (a • b : B) = a • (b : C) :=
calc
((a • b : B) : C) = (a • b) • 1 := Algebra.algebraMap_eq_smul_one _
_ = a • (b • 1) := smul_assoc ..
_ = a • (b : C) := congrArg _ (Algebra.algebraMap_eq_smul_one b).symm
