star_mem — Mathlib

English

The star membership criterion in spinGroup is equivalent to ordinary membership.

Русский

Критерий принадлежности через звезду в spinGroup эквивалентен обычному членству.

LaTeX

$$star_mem_iff {x : CliffordAlgebra Q} : star x ∈ spinGroup Q ↔ x ∈ spinGroup Q$$

Lean4

/-- See `star_mem_iff` for both directions. -/
theorem star_mem {x : CliffordAlgebra Q} (hx : x ∈ spinGroup Q) : star x ∈ spinGroup Q :=
  by
  rw [mem_iff] at hx ⊢
  obtain ⟨hx₁, hx₂⟩ := hx
  refine ⟨pinGroup.star_mem hx₁, ?_⟩
  dsimp only [CliffordAlgebra.even] at hx₂ ⊢
  simp only [Submodule.mem_toSubalgebra] at hx₂ ⊢
  simp only [star_def, reverse_mem_evenOdd_iff, involute_mem_evenOdd_iff, hx₂]

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