star_mem — Mathlib

English

The star operation on the pinGroup inherits a Star structure from the ambient Clifford algebra, making pinGroup a star-subtype within the monoid.

Русский

Операция звезды на pinGroup наследует структуру звезды из окружной CliffordAlgebra, образуя-star-подмножество внутри моноида.

LaTeX

$$$$\\text{instance: } \\text{Star}(\\text{pinGroup}(Q)) \\text{ defined by } x \\mapsto \\star x.$$$$

Lean4

/-- See `star_mem_iff` for both directions. -/
theorem star_mem {x : CliffordAlgebra Q} (hx : x ∈ pinGroup Q) : star x ∈ pinGroup Q :=
  by
  rw [mem_iff] at hx ⊢
  refine ⟨?_, unitary.star_mem hx.2⟩
  rcases hx with ⟨⟨y, hy₁, hy₂⟩, _hx₂, hx₃⟩
  simp only [Subgroup.coe_toSubmonoid, SetLike.mem_coe] at hy₁
  simp only [Units.coeHom_apply] at hy₂
  simp only [Submonoid.mem_map, Subgroup.mem_toSubmonoid, Units.coeHom_apply]
  refine ⟨star y, ?_, by simp only [hy₂, Units.coe_star]⟩
  rw [← hy₂] at hx₃
  have hy₃ : y * star y = 1 := by
    rw [← Units.val_inj]
    simp only [hx₃, Units.val_mul, Units.coe_star, Units.val_one]
  apply_fun fun x => y⁻¹ * x at hy₃
  simp only [inv_mul_cancel_left, mul_one] at hy₃
  simp only [hy₃, hy₁, inv_mem_iff]

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