Facts about ordered structures and ordered instances on subgroups

@[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} : mabs x ∈ H ↔ x ∈ H

@[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

instance instIsModularLatticeSubgroup {C : Type u_1} [CommGroup C] : IsModularLattice (Subgroup C)

instance instIsModularLatticeAddSubgroup {C : Type u_1} [AddCommGroup C] : IsModularLattice (AddSubgroup C)

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

@[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

@[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

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)

instance Subgroup.toIsOrderedMonoid {G : Type u_1} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] (H : Subgroup G) : IsOrderedMonoid ↥H

A subgroup of an ordered group is an ordered group.

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

An AddSubgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

theorem Subsemigroup.strictMono_topEquiv {G : Type u_1} [CommMonoid G] [PartialOrder G] : StrictMono ⇑topEquiv

theorem AddSubsemigroup.strictMono_topEquiv {G : Type u_1} [AddCommMonoid G] [PartialOrder G] : StrictMono ⇑topEquiv

theorem MulEquiv.strictMono_subsemigroupCongr {G : Type u_1} [CommMonoid G] [PartialOrder G] {S T : Subsemigroup G} (h : S = T) : StrictMono ⇑(subsemigroupCongr h)

theorem AddEquiv.strictMono_subsemigroupCongr {G : Type u_1} [AddCommMonoid G] [PartialOrder G] {S T : AddSubsemigroup G} (h : S = T) : StrictMono ⇑(subsemigroupCongr h)

theorem MulEquiv.strictMono_symm {G : Type u_1} {G' : Type u_2} [CommMonoid G] [LinearOrder G] [CommMonoid G'] [PartialOrder G'] {e : G ≃* G'} (he : StrictMono ⇑e) : StrictMono ⇑e.symm

theorem AddEquiv.strictMono_symm {G : Type u_1} {G' : Type u_2} [AddCommMonoid G] [LinearOrder G] [AddCommMonoid G'] [PartialOrder G'] {e : G ≃+ G'} (he : StrictMono ⇑e) : StrictMono ⇑e.symm