smul_coe — Mathlib

English

Let a be a unit in R and x be a nonzero element of M. The action of a on x, viewed in the ambient monoid M, agrees with applying a to the value of x on the ambient type: (a • x).val = a • x.val.

Русский

Пусть a ∈ R^× и x ∈ { m ∈ M | m ≠ 0 }. Тогда значение bajo действия a над x в подтипе совпадает со значением действия a над x в M: (a • x).val = a • x.val.

LaTeX

$$$ (a \\cdot x)_{\\mathrm{val}} = a \\cdot x_{\\mathrm{val}} $$$

Lean4

@[simp]
theorem smul_coe (a : Rˣ) (x : { x : M // x ≠ 0 }) : (a • x).val = a • x.val :=
  rfl

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