mem_iff

Mathlib.Algebra.Star.Unitary

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

English

An element U lies in unitary R iff star U · U = 1 and U · star U = 1.

Русский

Элемент U принадлежит unitary R тогда и только тогда, когда star U · U = 1 и U · star U = 1.

LaTeX

$$$ U \in \mathrm{unitary}(R) \iff \star U \cdot U = 1 \land U \cdot \star U = 1 $$$

Lean4

theorem mem_iff {U : R} : U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1 :=
  Iff.rfl

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

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

Разделы

Аффилиация

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