mem_iff — Mathlib

English

If x lies in the pin group, then star x also lies in the pin group.

Русский

Если x принадлежит pinGroup, то star x тоже принадлежит pinGroup.

LaTeX

$$$$\\forall x \\in \\mathrm{pinGroup}(Q),\\ star x \\in \\mathrm{pinGroup}(Q).$$$$

Lean4

/-- An element is in `pinGroup Q` if and only if it is in `lipschitzGroup Q` and `unitary`. -/
theorem mem_iff {x : CliffordAlgebra Q} :
    x ∈ pinGroup Q ↔
      x ∈ (lipschitzGroup Q).toSubmonoid.map (Units.coeHom <| CliffordAlgebra Q) ∧ x ∈ unitary (CliffordAlgebra Q) :=
  Iff.rfl

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