star_eq

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#IsSelfAdjoint.star_eq

English

If an element is self-adjoint, then star x = x.

Русский

Если элемент самопряжён, то star x = x.

LaTeX

$$$IsSelfAdjoint x \\Rightarrow \\ star x = x.$$$

Lean4

theorem star_eq [Star R] {x : R} (hx : IsSelfAdjoint x) : star x = x :=
  hx

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

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

Разделы

Аффилиация

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