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
AddSubmonoidClass.instAddArchimedean
{M : Type u_1}
{S : Type u_2}
[SetLike S M]
[OrderedAddCommMonoid M]
[AddSubmonoidClass S M]
[Archimedean M]
(H : S)
:
Archimedean { x : M // x ∈ H }
Equations
- ⋯ = ⋯
instance
SubmonoidClass.instMulArchimedean
{M : Type u_1}
{S : Type u_2}
[SetLike S M]
[OrderedCommMonoid M]
[SubmonoidClass S M]
[MulArchimedean M]
(H : S)
:
MulArchimedean { x : M // x ∈ H }
Equations
- ⋯ = ⋯