star_mul_self

Mathlib.Algebra.Star.SelfAdjoint

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

English

The product star x · x is self-adjoint for any x.

Русский

Произведение star x и x является самосопряжённым для любого x.

LaTeX

$$$IsSelfAdjoint (star x \\cdot x).$$$

Lean4

@[simp]
theorem star_mul_self [Mul R] [StarMul R] (x : R) : IsSelfAdjoint (star x * x) := by
  simp only [IsSelfAdjoint, star_mul, star_star]

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

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

Разделы

Аффилиация

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