conjAct_smul_range_ι — Mathlib

English

The conjugation action by x in pinGroup Q sends ι Q m to the range of ι Q.

Русский

Действие конъюгации x в pinGroup Q отправляет ι_Q m в диапазон ι_Q.

LaTeX

$$$$\\forall x\\in \\mathrm{pinGroup}(Q),\\ ConjAct.toConjAct x \\cdot ι_Q(m) \\in \\mathrm{range}(ι_Q).$$$$

Lean4

/-- If x is in `pinGroup Q`, then `(ι Q).range` is closed under twisted conjugation. The reverse
statement presumably being true only in finite dimensions. -/
theorem conjAct_smul_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : ↑x ∈ pinGroup Q) [Invertible (2 : R)] :
    ConjAct.toConjAct x • LinearMap.range (ι Q) = LinearMap.range (ι Q) :=
  lipschitzGroup.conjAct_smul_range_ι (units_mem_lipschitzGroup hx)

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