isStarNormal_of_mem_unitary

Mathlib.Algebra.Star.Unitary

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

← MathLib Explorer

English

If u ∈ unitary(R), then IsStarNormal u.

Русский

Если u ∈ unitary(R), то IsStarNormal u.

LaTeX

$$$ u \in \mathrm{unitary}(R) \Rightarrow \mathrm{IsStarNormal}(u) $$$

Lean4

@[aesop 10% apply (rule_sets := [CStarAlgebra])]
theorem _root_.isStarNormal_of_mem_unitary {u : R} (hu : u ∈ unitary R) : IsStarNormal u :=
  coe_isStarNormal ⟨u, hu⟩

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

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

Разделы

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

Аффилиация

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