instIsStrictOrderedRing — Mathlib

English

If β is a Semiring with a strict order (IsStrictOrderedRing), then Germ β is a IsStrictOrderedRing.

Русский

Если β — строгопорядковое кольцо (IsStrictOrderedRing), то Germ β — тоже строго упорядченное кольцо.

LaTeX

$$$\\text{IsStrictOrderedRing}(β, \\le) \\Rightarrow \\text{IsStrictOrderedRing}(β^*, \\le).$$$

Lean4

instance instIsStrictOrderedRing [Semiring β] [PartialOrder β] [IsStrictOrderedRing β] : IsStrictOrderedRing β*
    where
  mul_lt_mul_of_pos_left x y
    z :=
    inductionOn₃ x y z fun _f _g _h hfg hh ↦
      coe_lt.2 <| (coe_lt.1 hh).mp <| (coe_lt.1 hfg).mono fun _a ↦ mul_lt_mul_of_pos_left
  mul_lt_mul_of_pos_right x y
    z :=
    inductionOn₃ x y z fun _f _g _h hfg hh ↦
      coe_lt.2 <| (coe_lt.1 hh).mp <| (coe_lt.1 hfg).mono fun _a ↦ mul_lt_mul_of_pos_right

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