star_mem_iff — Mathlib

English

Two-way equivalence between membership of star x in pinGroup and membership of x in pinGroup.

Русский

Двустороннее эквивалентность принадлежности star x к pinGroup и принадлежности самого x к pinGroup.

LaTeX

$$$$\\text{star\_mem\_iff} : star x \\in \\mathrm{pinGroup}(Q) \\iff x \\in \\mathrm{pinGroup}(Q).$$$$

Lean4

/-- An element is in `pinGroup Q` if and only if `star x` is in `pinGroup Q`.
See `star_mem` for only one direction. -/
@[simp]
theorem star_mem_iff {x : CliffordAlgebra Q} : star x ∈ pinGroup Q ↔ x ∈ pinGroup Q :=
  by
  refine ⟨?_, star_mem⟩
  intro hx
  convert star_mem hx
  exact (star_star x).symm

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