instLinearOrderOfIsOrderedCancelMonoid

English

If α is a linear order and an ordered cancellative monoid, then Localization(s) is endowed with a linear order extending the original order, with the totality of comparisons.

Русский

Если α — линейный порядок и упорядоченный отменяющий моноид, то у Localization(s) появляется линейный порядок, расширяющий исходный порядок и обеспечивающий полноту сравнений.

LaTeX

$$$\\text{LinearOrder}(\\operatorname{Localization}(s))$$$

Lean4

@[to_additive]
instance [CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : LinearOrder (Localization s) :=
  { le_total := fun a b =>
      Localization.induction_on₂ a b fun _ _ => by
        simp_rw [mk_le_mk]
        exact le_total _ _
    toDecidableLE := Localization.decidableLE
    toDecidableLT := Localization.decidableLT
    toDecidableEq := Localization.decidableEq }

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