coe_smul — Mathlib

English

For any a ∈ R≥0 and x ∈ S, the action of a considered as an element of R agrees with its action as an R≥0-scalar: (a) • x = a • x.

Русский

Для любого a ∈ R≥0 и x ∈ S, действие a как элемента R совпадает с действием как скаляра R≥0: (a) • x = a • x.

LaTeX

$$$ (a : \\mathbb{R}) \\cdot x = a \\cdot x $$$

Lean4

@[simp, norm_cast]
theorem coe_smul (a : R≥0) (x : S) : (a : R) • x = a • x :=
  rfl

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