linearOrderedCommMonoidWithZero — Mathlib

English

The nonnegative subtype { x ∈ α | 0 ≤ x } inherits a LinearOrderedCommMonoidWithZero structure from α.

Русский

Неотрицательный подтип { x ∈ α | 0 ≤ x } наследует структуру линейно упорядоченного коммутативного моноида с нулём от α.

LaTeX

$$$\\text{LinearOrderedCommMonoidWithZero}\\, \\{ x : \\alpha \\mid 0 \\le x \\}$$$

Lean4

instance linearOrderedCommMonoidWithZero [CommSemiring α] [LinearOrder α] [IsStrictOrderedRing α] :
    LinearOrderedCommMonoidWithZero { x : α // 0 ≤ x } :=
  { Nonneg.commSemiring, Nonneg.isOrderedRing with mul_le_mul_left := fun _ _ h c ↦ mul_le_mul_of_nonneg_left h c.prop }

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