isOrderedCancelMonoid — Mathlib

English

The localization Localization(s) forms an ordered cancellative monoid: the natural order is compatible with multiplication and cancellation, so inequalities are preserved under left multiplication and cancellation holds.

Русский

Локализация Localization(s) образует упорядоченный отменяющий моноид: естественный порядок совместим с умножением и отменой, и неравенства сохраняются при левом умножении, а отмена справедлива.

LaTeX

$$$\\operatorname{IsOrderedCancelMonoid}(\\operatorname{Localization}(s))$$$

Lean4

@[to_additive]
instance isOrderedCancelMonoid : IsOrderedCancelMonoid (Localization s)
    where
  mul_le_mul_left := fun a b =>
    Localization.induction_on₂ a b fun a b hab c =>
      Localization.induction_on c fun c =>
        by
        simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ _ c.1] at hab ⊢
        exact mul_le_mul_left' hab _
  le_of_mul_le_mul_left := fun a b c =>
    Localization.induction_on₃ a b c fun a b c hab =>
      by
      simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ _ a.1] at hab ⊢
      exact le_of_mul_le_mul_left' hab

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