Documentation

Mathlib.Algebra.Group.Subgroup.Order

Facts about ordered structures and ordered instances on subgroups #

source
@[simp]
theorem mabs_mem_iff {S : Type u_1} {G : Type u_2} [Group G] [LinearOrder G] {x✝ : SetLike S G} [InvMemClass S G] {H : S} {x : G} :
|x|ₘ ∈ H ↔ x ∈ H
source
@[simp]
theorem abs_mem_iff {S : Type u_1} {G : Type u_2} [AddGroup G] [LinearOrder G] {x✝ : SetLike S G} [NegMemClass S G] {H : S} {x : G} :
|x| ∈ H ↔ x ∈ H
source
instance instIsModularLatticeSubgroup {C : Type u_1} [CommGroup C] :
IsModularLattice (Subgroup C)
source
instance instIsModularLatticeAddSubgroup {C : Type u_1} [AddCommGroup C] :
IsModularLattice (AddSubgroup C)
source
theorem Subgroup.NormalizerCondition.normal_of_coatom {G : Type u_1} [Group G] (H : Subgroup G) (hnc : NormalizerCondition G) (hmax : IsCoatom H) :
H.Normal

In a group that satisfies the normalizer condition, every maximal subgroup is normal

source
theorem AddSubgroup.NormalizerCondition.normal_of_coatom {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (hnc : AddNormalizerCondition G) (hmax : IsCoatom H) :
H.Normal

In an additive group that satisfies the normalizer condition, every maximal additive subgroup is normal

source
@[simp]
theorem Subgroup.isCoatom_comap {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G ≃* H) {K : Subgroup H} :
IsCoatom (comap (↑f) K) ↔ IsCoatom K
source
@[simp]
theorem Subgroup.isCoatom_map {G : Type u_1} [Group G] (H : Subgroup G) (f : G ≃* ↥H) {K : Subgroup G} :
IsCoatom (map (↑f) K) ↔ IsCoatom K
source
theorem Subgroup.isCoatom_comap_of_surjective {G : Type u_1} [Group G] {H : Type u_2} [Group H] {φ : G →* H} (hφ : Function.Surjective ⇑φ) {M : Subgroup H} (hM : IsCoatom M) :
IsCoatom (comap φ M)
source
instance Subgroup.toIsOrderedMonoid {G : Type u_1} [CommGroup G] [Preorder G] [IsOrderedMonoid G] (H : Subgroup G) :
IsOrderedMonoid ↥H

A subgroup of an ordered group is an ordered group.

source
instance AddSubgroup.toIsOrderedAddMonoid {G : Type u_1} [AddCommGroup G] [Preorder G] [IsOrderedAddMonoid G] (H : AddSubgroup G) :
IsOrderedAddMonoid ↥H

An additive subgroup of an additive ordered group is an additive ordered group.

source
theorem Subsemigroup.strictMono_topEquiv {G : Type u_1} [CommMonoid G] [Preorder G] :
StrictMono ⇑topEquiv
source
theorem AddSubsemigroup.strictMono_topEquiv {G : Type u_1} [AddCommMonoid G] [Preorder G] :
StrictMono ⇑topEquiv
source
theorem MulEquiv.strictMono_subsemigroupCongr {G : Type u_1} [CommMonoid G] [Preorder G] {S T : Subsemigroup G} (h : S = T) :
StrictMono ⇑(subsemigroupCongr h)
source
theorem AddEquiv.strictMono_subsemigroupCongr {G : Type u_1} [AddCommMonoid G] [Preorder G] {S T : AddSubsemigroup G} (h : S = T) :
StrictMono ⇑(subsemigroupCongr h)
source
theorem MulEquiv.strictMono_symm {G : Type u_1} {G' : Type u_2} [CommMonoid G] [LinearOrder G] [CommMonoid G'] [Preorder G'] {e : G ≃* G'} (he : StrictMono ⇑e) :
StrictMono ⇑e.symm
source
theorem AddEquiv.strictMono_symm {G : Type u_1} {G' : Type u_2} [AddCommMonoid G] [LinearOrder G] [AddCommMonoid G'] [Preorder G'] {e : G ≃+ G'} (he : StrictMono ⇑e) :
StrictMono ⇑e.symm