mem_unitary — Mathlib

English

If a unit belongs to pinGroup, then its underlying unit lies in LipschitzGroup.

Русский

Если единица принадлежит pinGroup, то соответствующая единица лежит в LipschitzGroup.

LaTeX

$$$$\\forall x : (CliffordAlgebra Q)^{\\times},\\ x \\in \\mathrm{pinGroup}(Q) \\Rightarrow x \\in \\mathrm{lipschitzGroup}(Q).$$$$

Lean4

theorem mem_unitary {x : CliffordAlgebra Q} (hx : x ∈ pinGroup Q) : x ∈ unitary (CliffordAlgebra Q) :=
  hx.2

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