conjugate'

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#IsSelfAdjoint.conjugate'

← MathLib Explorer

English

If x is self-adjoint, star z x z is self-adjoint for any z.

Русский

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

LaTeX

$$$\text{IsSelfAdjoint}(\star z \cdot x \cdot z)$$$

Lean4

@[aesop safe apply]
theorem conjugate' {x : R} (hx : IsSelfAdjoint x) (z : R) : IsSelfAdjoint (star z * x * z) := by
  simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]

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

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

Разделы

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

Аффилиация

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