conjugate_le_conjugate — Mathlib

English

If a ≤ b, then star c · a · c ≤ star c · b · c for any c.

Русский

Если a ≤ b, то star c · a · c ≤ star c · b · c для любого c.

LaTeX

$$$a \le b \Rightarrow \star c \cdot a \cdot c \le \star c \cdot b \cdot c$$$

Lean4

theorem conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) : star c * a * c ≤ star c * b * c :=
  by
  rw [StarOrderedRing.le_iff] at hab ⊢
  obtain ⟨p, hp, rfl⟩ := hab
  simp_rw [← StarOrderedRing.nonneg_iff] at hp ⊢
  exact ⟨star c * p * c, conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩

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