inv_mem

Mathlib.Algebra.Star.Unitary

URI: https://scilib.ai/kg/mathlib#unitary.inv_mem

← MathLib Explorer

English

If g ∈ G is unitary, then g^{-1} ∈ unitary(G).

Русский

Если g ∈ G является унитарным, то g^{-1} ∈ unitary(G).

LaTeX

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

Lean4

theorem inv_mem {g : G} (hg : g ∈ unitary G) : g⁻¹ ∈ unitary G :=
  by
  simp_rw [unitary.mem_iff, star_inv, ← mul_inv_rev, inv_eq_one] at *
  exact hg.symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru