conjAct_smul_ι_mem_range_ι — Mathlib

English

Conjugation by elements of spinGroup Q preserves the space spanned by ι Q.

Русский

Через конъюгацию элементами spinGroup Q сохраняется образ пространства, порождаемого ι Q.

LaTeX

$$ConjAct.toConjAct x • ι Q y ∈ range (ι Q)$$

Lean4

/-- The conjugation action by elements of the spin group keeps vectors as vectors. -/
theorem conjAct_smul_ι_mem_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : ↑x ∈ spinGroup Q) [Invertible (2 : R)] (y : M) :
    ConjAct.toConjAct x • ι Q y ∈ LinearMap.range (ι Q) :=
  lipschitzGroup.conjAct_smul_ι_mem_range_ι (units_mem_lipschitzGroup hx) y

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