English
If α and β are R-modules and e: α ≃ₗ[R] β is a linear equivalence, then the transported module structure on α yields a valid IsScalarTower R A α: scalar actions commute along the tower.
Русский
Если α и β модули над R и есть линейное эквивалентность e: α ≃ₗ[R] β, то перенос модуля на α образует допустимое IsScalarTower R A α: действия скаляров согласованы по башне.
LaTeX
$$$\\text{IsScalarTower } R A α$ given $e: α \\simeq_ℓ[R] β$$$
Lean4
/-- The module instance from `AddEquiv.module` is compatible with the `R`-module structures,
if the `AddEquiv` is induced by an `R`-module isomorphism. -/
theorem isScalarTower [Module R α] [Module R β] [IsScalarTower R A β] (e : α ≃ₗ[R] β) :
letI := e.toAddEquiv.module A
IsScalarTower R A α :=
by
letI := e.toAddEquiv.module A
constructor
intro x y z
simp only [Equiv.smul_def, smul_assoc]
apply e.symm.map_smul
