posMulReflectLE_iff_mulPosReflectLE

English

PosMulReflectLE α is equivalent to MulPosReflectLE α under commutativity assumptions.

Русский

PosMulReflectLE α эквивалентно MulPosReflectLE α при предположении коммутативности.

LaTeX

$$$\\\\forall α\\,[Mul α][Zero α][Preorder α]\\ [Std.Commutative (\\cdot)],\\\\\\\\ PosMulReflectLE α \\leftrightarrow MulPosReflectLE α.$$$

Lean4

theorem posMulReflectLE_iff_mulPosReflectLE : PosMulReflectLE α ↔ MulPosReflectLE α := by
  simp only [posMulReflectLE_iff, mulPosReflectLE_iff, Std.Commutative.comm]

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