English
A version of involute_act_ι_mem_range_ι asserting the same range-closure property using involute on x.
Русский
Версия involute_act_ι_mem_range_ι, утверждающая такое же свойство сохранения диапазона через инволюцию.
LaTeX
$$$$lipschitzGroup.InvoluteAct_ι_mem_range_ι(Q, x, m)$$$$
Lean4
/-- This is another version of `conjAct_smul_ι_mem_range_ι` which uses `involute`. -/
theorem involute_act_ι_mem_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : ↑x ∈ pinGroup 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