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] [CommMonoid M] [PartialOrder M] [SubmonoidClass S M] [MulArchimedean M] (H : S) :
instance AddSubmonoidClass.instAddArchimedean {M : Type u_1} {S : Type u_2} [SetLike S M] [AddCommMonoid M] [PartialOrder M] [AddSubmonoidClass S M] [Archimedean M] (H : S) :
Archimedean ↥H