toPosMulStrictMono — Mathlib

English

There is a CharZero structure on any AddMonoidWithOne R that satisfies the usual order properties, provided noZeroDivisors and nontriviality hold.

Русский

Для любого AddMonoidWithOne R существует структура CharZero, удовлетворяющая обычным свойствам порядка при отсутствии нулевых делителей и ненулевости.

LaTeX

$$$ \\forall R [AddMonoidWithOne R] [PartialOrder R] [ZeroLEOneClass R] [\\text{NeZero }(1:\\,R)] [AddLeftStrictMono R],\\; \\text{CharZero } R. $$$

Lean4

instance (priority := 200) toPosMulStrictMono : PosMulStrictMono R where
  elim x _ _ h := IsStrictOrderedRing.mul_lt_mul_of_pos_left _ _ _ h x.prop

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