units_mem_lipschitzGroup — Mathlib

English

Conjugation by any element of the Lipschitz group acts on ι Q m by staying inside the range of ι Q.

Русский

Конъугирование элементами LipschitzGroup отображает ι_Q m в образ ι_Q.

LaTeX

$$$$\\forall x\\in \\mathrm{lipschitzGroup}(Q),\\ ConjAct.toConjAct x \\cdot (\\iota_Q m) \\in \\mathrm{range}(\\iota_Q). $$$$

Lean4

theorem units_mem_lipschitzGroup {x : (CliffordAlgebra Q)ˣ} (hx : ↑x ∈ pinGroup Q) : x ∈ lipschitzGroup Q :=
  (units_mem_iff.1 hx).1

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