instOrderTop — Mathlib

English

In a commutative monoid with zero, the order on Associates has top equal to 0, i.e., a ≤ 0 for all a.

Русский

В коммутативном моноиде с нулём порядок на Associates имеет верхнюю границу, равную 0; то есть для всякого a выполняется a ≤ 0.

LaTeX

$$$ \forall a \in \mathrm{Associates}(M),\ a \le 0 $$$

Lean4

instance instOrderTop : OrderTop (Associates M) where
  top := 0
  le_top := dvd_zero

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