coe_smul_of_tower — Mathlib

English

The equalities of scalar actions are preserved when passing through towers.

Русский

Сохранение равенств скалярных действий при переходе через каскады.

LaTeX

$$$ [SMul S R] [SMul S M] [IsScalarTower S R M] (r: S) (x: p) : ((r • x) : M) = r • (x : M)$$$

Lean4

@[simp, norm_cast]
theorem coe_smul_of_tower [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : p) :
    ((r • x : p) : M) = r • (x : M) :=
  rfl

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