English
Another version for the special case c2 = 0: star (s • a) = s • star a.
Русский
Еще одна версия для специального случая c2 = 0: star (s • a) = s • star a.
LaTeX
$$$\star (s \cdot a) = s \cdot \star a$$$
Lean4
/-- A version of `star_smul` for the special case when `c₂ = 0`, without `SMulCommClass S R R`. -/
theorem star_smul' [Monoid S] [DistribMulAction S R] (s : S) (a : ℍ[R,c₁,0,c₃]) : star (s • a) = s • star a :=
QuaternionAlgebra.ext (by simp) (smul_neg _ _).symm (smul_neg _ _).symm (smul_neg _ _).symm