commute_iff_mul_nonneg — Mathlib

English

Two positive elements commute if and only if their product is nonnegative.

Русский

Два неотрицательных элемента коммутируют тогда и только тогда, когда их произведение неотрицательно.

LaTeX

$$$$ a,b \\ge 0 \\Rightarrow (Commute(a,b) \\iff 0 \\le a b) $$$$

Lean4

theorem commute_iff_mul_nonneg {a b : A} (ha : 0 ≤ a) (hb : 0 ≤ b) : Commute a b ↔ 0 ≤ a * b :=
  ⟨Commute.mul_nonneg ha hb, fun h => ha.isSelfAdjoint.commute_iff hb.isSelfAdjoint |>.mpr h.isSelfAdjoint⟩

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