instLinearOrder — Mathlib

English

There is a LinearOrder instance on MulArchimedeanClass M when M is a CommGroup with LinearOrder and IsOrderedMonoid.

Русский

Существует линейный порядок на MulArchimedeanClass M, если M — коммутативная группа с линейным порядком и условием упорядоченного моноида.

LaTeX

$$LinearOrder (MulArchimedeanClass M)$$

Lean4

@[to_additive]
noncomputable instance : LinearOrder (MulArchimedeanClass M) := by
  classical
  unfold MulArchimedeanClass
  infer_instance

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