isStrictOrderedRing — Mathlib

English

If α has IsStrictOrderedRing, then the nonnegative subtype inherits IsStrictOrderedRing.

Русский

Если α обладает IsStrictOrderedRing, то неотрицательный подтип наследует IsStrictOrderedRing.

LaTeX

$$$ IsStrictOrderedRing\\, \\{ x : \\alpha \\mid 0 \\le x \\} $$$

Lean4

instance isStrictOrderedRing [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] :
    IsStrictOrderedRing { x : α // 0 ≤ x } :=
  Function.Injective.isStrictOrderedRing Subtype.val Nonneg.coe_zero Nonneg.coe_one Nonneg.coe_add Nonneg.coe_mul .rfl
    .rfl

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