val_smul_of_tower — Mathlib

English

The action on the subtype s is compatible with the ambient α-action: the α-image of r•x equals r•(x) for x ∈ s.

Русский

Действие над подтипом s совместимо с действием над α: образ α от r•x равен r•(образ x) при x ∈ s.

LaTeX

$$$\\forall (r \\in M) (x \\in s): \\; (\\uparrow (r \\cdot x) : \\alpha) = r \\cdot (x : \\alpha)$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
protected theorem val_smul_of_tower (r : M) (x : s) : (↑(r • x) : α) = r • (x : α) :=
  rfl

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