mem_unitarySubgroup_iff — Mathlib

English

In a group equipped with an involution, the unitary subgroup coincides with the set of unitary elements; for every element g, g lies in the unitary subgroup of G if and only if g is unitary in G.

Русский

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

LaTeX

$$$\\forall g\\in G:\\, g\\in\\mathrm{unitarySubgroup}(G) \\iff g\\in\\mathrm{unitary}(G)$$$

Lean4

@[simp]
theorem mem_unitarySubgroup_iff {g : G} : g ∈ unitarySubgroup G ↔ g ∈ unitary G :=
  Iff.rfl

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