inv_mem_iff — Mathlib

English

In a group with involution, the inverse of a unitary element is unitary if and only if the original element is unitary.

Русский

В группе с инволюцией обратный к унитарному элементу тоже унитарен тогда и только тогда, когда сам элемент унитарен.

LaTeX

$$$g^{-1} \\in \\mathrm{unitary}(G) \\iff g \\in \\mathrm{unitary}(G)$$$

Lean4

nonrec theorem inv_mem_iff {g : G} : g⁻¹ ∈ unitary G ↔ g ∈ unitary G :=
  inv_mem_iff (H := unitarySubgroup G)

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