unitarySubgroup_toSubmonoid

Mathlib.Algebra.Star.Unitary

URI: https://scilib.ai/kg/mathlib#unitarySubgroup_toSubmonoid

English

The underlying submonoid of the unitary subgroup equals the unitary set.

Русский

Внутреннее подмоноид единиц совпадает с множеством унитарных элементов.

LaTeX

$$$ (\mathrm{unitarySubgroup}(G)).\mathrm{toSubmonoid} = \mathrm{unitary}(G) $$$

Lean4

@[simp]
theorem unitarySubgroup_toSubmonoid : (unitarySubgroup G).toSubmonoid = unitary G :=
  rfl

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

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

Разделы

Аффилиация

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