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