star_smul' — Mathlib

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

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