involute_act_ι_mem_range_ι — Mathlib

English

The involute action by units of CliffordAlgebra acts on ι Q y yielding something in the range of ι Q.

Русский

Действие involute единицы CliffordAlgebra на ι Q y производит элемент, принадлежащий диапазону ι Q.

LaTeX

$$involute (Q := Q) ↑x * ι Q y * ↑x⁻¹ ∈ range (ι Q)$$

Lean4

theorem involute_act_ι_mem_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : ↑x ∈ spinGroup Q) [Invertible (2 : R)] (y : M) :
    involute (Q := Q) ↑x * ι Q y * ↑x⁻¹ ∈ LinearMap.range (ι Q) :=
  lipschitzGroup.involute_act_ι_mem_range_ι (units_mem_lipschitzGroup hx) y

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