isStarNormal_of_mem

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#skewAdjoint.isStarNormal_of_mem

← MathLib Explorer

English

If x is skew-adjoint, then x is star-normal.

Русский

Если x — кососопряжённый элемент, то он звездно-нормален.

LaTeX

$$$ \\forall x \\in \\mathrm{R}, \\; x \\text{ skewAdjoint} \\Rightarrow \\mathrm{IsStarNormal}(x). $$$

Lean4

theorem isStarNormal_of_mem {x : R} (hx : x ∈ skewAdjoint R) : IsStarNormal x :=
  ⟨by
    simp only [mem_iff] at hx
    simp only [hx, Commute.neg_left, Commute.refl]⟩

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

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

Разделы

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

Аффилиация

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