conjAct_smul_ι_mem_range_ι — Mathlib

English

Using the involute, the image of an element of pinGroup under conjugation-like action remains in the range of ι Q.

Русский

Используя инволюцию, образ элемента pinGroup при действии аналогичном конъюгации остаётся в диапазоне ι_Q.

LaTeX

$$$$involute( Q := Q)\\ (↑x) \\cdot ι_Q(m) \\cdot ↑x^{-1} \\in \\mathrm{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 ∈ pinGroup Q) [Invertible (2 : R)] (y : M) :
    ConjAct.toConjAct x • ι Q y ∈ LinearMap.range (ι Q) :=
  lipschitzGroup.conjAct_smul_ι_mem_range_ι (units_mem_lipschitzGroup hx) y

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