instOrderTop — Mathlib

English

The Archimedean class of 1 is the top element in MulArchimedeanClass M.

Русский

Архимедов класс числа 1 является верхним элементом в MulArchimedeanClass M.

LaTeX

$$$\top = mk\ 1$$$

Lean4

/-- 1 is in its own class (see `MulArchimedeanClass.mk_eq_top_iff`),
which is also the largest class. -/
@[to_additive /-- 0 is in its own class (see `ArchimedeanClass.mk_eq_top_iff`),
    which is also the largest class. -/
    ]
instance : OrderTop (MulArchimedeanClass M) where
  top := mk 1
  le_top
    A :=
    by
    induction A using ind with
    | mk a
    rw [mk_le_mk]
    exact ⟨1, by simp⟩

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