instOrd — Mathlib

English

There is an order on Units α given by compare a b := compare a.val b.val; i.e., Units inherits its order from α via val.

Русский

Существует порядок на единицах α, задаваемый compare a b := compare a.val b.val; то есть Units наследует порядок от α через val.

LaTeX

$$$\\forall a,b \\in \\mathrm{Units}(\\alpha),\\ \\mathrm{Ord}_{\\mathrm{Units}(\\alpha)}: \\mathrm{compare}_{\\mathrm{Units}}(a,b) = \\mathrm{compare}_{\\alpha}(a.\\mathrm{val}, b.\\mathrm{val})$$$

Lean4

@[to_additive]
instance [Monoid α] [Ord α] : Ord αˣ where compare a b := compare a.val b.val

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