Submonoids of archimedean monoids

This file defines the instances that show that the (mul)archimedean property is retained in a submonoid of the ambient group.

Main statements

• SubmonoidClass.instMulArchimedean: the submonoid (and similar subobjects) of a mul-archimedean group retains the mul-archimedean property when restricted to the submonoid.
• AddSubmonoidClass.instArchimedean: the additive submonoid (and similar subobjects) of an archimedean additive group retains the archimedean property when restricted to the additive submonoid.

instance SubmonoidClass.instMulArchimedean {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCommMonoid M] [SubmonoidClass S M] [MulArchimedean M] (H : S) : MulArchimedean ↥H

Equations

• ⋯ = ⋯

instance AddSubmonoidClass.instAddArchimedean {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] [Archimedean M] (H : S) : Archimedean ↥H

Equations

• ⋯ = ⋯