star_mem

Mathlib.Algebra.Star.Unitary

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

← MathLib Explorer

English

If U is unitary, then star U is also unitary.

Русский

Если U — унитарен, то star U тоже унитарен.

LaTeX

$$$ U \in \mathrm{unitary}(R) \Rightarrow \star U \in \mathrm{unitary}(R) $$$

Lean4

theorem star_mem {U : R} (hU : U ∈ unitary R) : star U ∈ unitary R :=
  ⟨by rw [star_star, mul_star_self_of_mem hU], by rw [star_star, star_mul_self_of_mem hU]⟩

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

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

Разделы

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

Аффилиация

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