conjugate_nonneg

Mathlib.Algebra.Order.Star.Basic

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

← MathLib Explorer

English

If a ≥ 0, then c · a · star c ≥ 0 for any c.

Русский

Если a ≥ 0, тогда для любого c: c · a · star c ≥ 0.

LaTeX

$$$0 \le a \Rightarrow \forall c, \ 0 \le c \cdot a \cdot \star c$$$

Lean4

@[aesop 90% apply (rule_sets := [CStarAlgebra])]
protected theorem conjugate_nonneg {a : R} (ha : 0 ≤ a) {c : R} (hc : IsSelfAdjoint c) : 0 ≤ c * a * c := by
  nth_rewrite 2 [← hc]; exact conjugate_nonneg' ha c

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

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

Разделы

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

Аффилиация

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