_example

Mathlib.Algebra.Order.Ring.Star

URI: https://scilib.ai/kg/mathlib#StarOrderedRing._example

Lean4

example {R : Type*} [Semiring R] [PartialOrder R] [IsOrderedRing R] [StarRing R] [StarOrderedRing R] {x y : R}
    (hx : 0 ≤ x) (hy : 0 ≤ y) : x * y = y * x := by
  rw [← IsSelfAdjoint.of_nonneg (mul_nonneg hy hx), star_mul, IsSelfAdjoint.of_nonneg hx, IsSelfAdjoint.of_nonneg hy]
    /- This will be implied by the instance below, we only prove it to avoid duplicating the
    argument in the instance below for `mul_le_mul_of_nonneg_right`. -/

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

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

Разделы

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

Аффилиация

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