coe_smul — Mathlib

English

Coefficients commute with quaternion multiplication in a compatible way: ↑(s • r) = s • r in the quaternion sense.

Русский

Коэффициенты подчиняют совместно умножению в кватернионе: ↑(s•r) = s•(r) в ℍ[R].

LaTeX

$$$\\uparrow (s \\cdot r) \\;\\left( : \\mathbb{H}(R) \\right) = s \\cdot (r \\cdot : \\mathbb{H}(R))$$$

Lean4

@[simp, norm_cast]
theorem coe_smul [SMulZeroClass S R] (s : S) (r : R) : (↑(s • r) : ℍ[R]) = s • (r : ℍ[R]) :=
  QuaternionAlgebra.coe_smul _ _

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