posMulStrictMono_iff_mulPosStrictMono

English

PosMulStrictMono α is equivalent to MulPosStrictMono α for a commutative α with preorder.

Русский

PosMulStrictMono α эквивално MulPosStrictMono α при условии коммутативности и порядка.

LaTeX

$$$\\\\forall α\\,[Std.Commutative (\\cdot) ]\\, [PosMulStrictMono α]\\\\leftrightarrow MulPosStrictMono α.$$$

Lean4

theorem posMulStrictMono_iff_mulPosStrictMono : PosMulStrictMono α ↔ MulPosStrictMono α := by
  simp only [posMulStrictMono_iff, mulPosStrictMono_iff, Std.Commutative.comm]

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