involute_act_ι_mem_range_ι — Mathlib

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

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