conjugate_self

Mathlib.Algebra.Star.SelfAdjoint

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

← MathLib Explorer

English

If x is self-adjoint and z is self-adjoint, then z x z is self-adjoint.

Русский

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

LaTeX

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

Lean4

@[aesop 90% apply]
theorem conjugate_self {x : R} (hx : IsSelfAdjoint x) {z : R} (hz : IsSelfAdjoint z) : IsSelfAdjoint (z * x * z) := by
  nth_rewrite 2 [← hz]; exact conjugate hx z

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

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

Разделы

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

Аффилиация

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