instNontrivial — Mathlib

English

If M is nontrivial, then MulArchimedeanClass M is nontrivial; there exist two distinct Archimedean classes.

Русский

Если M не тривиален, то MulArchimedeanClass M тривиален не является; существуют две различные Архимедовы класса.

LaTeX

$$∀ {M}, [CommGroup M], [LinearOrder M], [IsOrderedMonoid M], [Nontrivial M],\ Nontrivial (MulArchimedeanClass M)$$

Lean4

@[to_additive]
instance [Nontrivial M] : Nontrivial (MulArchimedeanClass M) where
  exists_pair_ne := by
    obtain ⟨x, hx⟩ := exists_ne (1 : M)
    exact ⟨mk x, ⊤, mk_eq_top_iff.ne.mpr hx⟩

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