instArchimedean — Mathlib

English

If G is a commutative group with a partial order and MulArchimedean structure, then Archimedean property passes to the additive version Additive G.

Русский

Если G — коммутативная группа с частичным порядком и структурой MulArchimedean, то Архимедово свойство переходит к аддитивной версии Additive G.

LaTeX

$$$\\text{Archimedean}(G) \\Rightarrow \\text{Archimedean}(\\text{Additive } G).$$$

Lean4

instance instArchimedean [CommGroup G] [PartialOrder G] [MulArchimedean G] : Archimedean (Additive G) :=
  ⟨fun x _ hy ↦ MulArchimedean.arch x.toMul hy⟩

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