coe_star — Mathlib

English

The inclusion of spinGroup Q into CliffordAlgebra Q commutes with the star operation; i.e., the star of the image of x equals the image of the star of x.

Русский

Включение spinGroup(Q) в CliffordAlgebra(Q) коммутирует с операцией звезды: образ star x совпадает с звездой образа x.

LaTeX

$$$\uparrow(\operatorname{star}(x)) = \operatorname{star}(\uparrow(x))$ for all $x \in \operatorname{spinGroup}(Q)$.$$

Lean4

@[simp, norm_cast]
theorem coe_star {x : spinGroup Q} : ↑(star x) = (star x : CliffordAlgebra Q) :=
  rfl

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