instLinearOrder — Mathlib

English

There is a LinearOrder on Units α, derived from the existing order on α via val and the previously defined min, max, compare operations.

Русский

Существует линейный порядок на Units α, полученный из существующего порядка на α через val и ранее определенные min, max, compare.

LaTeX

$$$\\forall a,b \\in \\mathrm{Units}(\\alpha),\\ \\mathrm{LinearOrder}_{\\mathrm{Units}(\\alpha)} \\text{ is defined by } a \\le b \\iff a.\\mathrm{val} \\le b.\\mathrm{val}$$$

Lean4

@[to_additive]
instance [Monoid α] [LinearOrder α] : LinearOrder αˣ :=
  val_injective.linearOrder _ val_le_val val_lt_val min_val max_val compare_val

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