posMulMono_iff_posMulStrictMono — Mathlib

English

PosMulMono α is equivalent to PosMulStrictMono α for CancelMonoidWithZero α under a partial order.

Русский

PosMulMono α эквивалентно PosMulStrictMono α для CancelMonoidWithZero α при заданном частичном порядке.

LaTeX

$$$PosMulMono\, \alpha \Leftrightarrow PosMulStrictMono\, \alpha$$$

Lean4

theorem posMulMono_iff_posMulStrictMono : PosMulMono α ↔ PosMulStrictMono α :=
  ⟨@PosMulMono.toPosMulStrictMono α _ _, @PosMulStrictMono.toPosMulMono α _ _⟩

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