val_smul — Mathlib

English

The coercion preserves scalar multiplication on the skew-adjoint subtype, i.e., the value of r • x equals r • (x in the ambient type).

Русский

Коэрцирование сохраняет скалярное умножение на подтипе кососопряжённых: значение r • x равно r • (x в окружающем типе).

LaTeX

$$$ \\forall r \\in R, \\; \\forall x \\in \\mathrm{skewAdjoint}(A), \\; (r \\cdot x).val = r \\cdot (x.\\text{val}). $$$

Lean4

@[simp, norm_cast]
theorem val_smul [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) (x : skewAdjoint A) :
    ↑(r • x) = r • (x : A) :=
  rfl

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