instIsStarNormalValMemAddSubgroup

Mathlib.Algebra.Star.SelfAdjoint

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

English

If x is a skew-adjoint element represented as a subtype, then its underlying value is IsStarNormal.

Русский

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

LaTeX

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

Lean4

instance (x : skewAdjoint R) : IsStarNormal (x : R) :=
  isStarNormal_of_mem (SetLike.coe_mem _)

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

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

Разделы

Аффилиация

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