instPartialOrderUnits — Mathlib

English

There is a partial order on Units α induced by the map val: a ≤ b iff a.val ≤ b.val.

Русский

Единицы α образуют частичный порядок, наследуемый от α по отображению val: a ≤ b ⇔ a.val ≤ b.val.

LaTeX

$$$\\forall a,b \\in \\mathrm{Units}(\\alpha),\\ a \\le_{\\mathrm{Units}} b \\iff a_{\\mathrm{val}} \\le b_{\\mathrm{val}}$$$

Lean4

@[to_additive]
instance instPartialOrderUnits [Monoid α] [PartialOrder α] : PartialOrder αˣ :=
  PartialOrder.lift val val_injective

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