star_mem_iff — Mathlib

English

The membership equivalence for unitary is preserved under star and back.

Русский

Эквивалентность принадлежности к unitary сохраняется после применения star и обратного преобразования.

LaTeX

$$$ U \in \mathrm{unitary}(R) \iff \star U \in \mathrm{unitary}(R) $$$

Lean4

@[simp]
theorem star_mem_iff {U : R} : star U ∈ unitary R ↔ U ∈ unitary R :=
  ⟨fun h => star_star U ▸ star_mem h, star_mem⟩

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