Facts about ordered structures and ordered instances on subgroups

@[simp]

theorem abs_mem_iff {S : Type u_1} {G : Type u_2} [AddGroup G] [LinearOrder G] : ∀ {x : SetLike S G} [inst : NegMemClass S G] {H : S} {x_1 : G}, |x_1| ∈ H ↔ x_1 ∈ H

@[simp]

theorem mabs_mem_iff {S : Type u_1} {G : Type u_2} [Group G] [LinearOrder G] : ∀ {x : SetLike S G} [inst : InvMemClass S G] {H : S} {x_1 : G}, mabs x_1 ∈ H ↔ x_1 ∈ H

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 (Subgroup.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 (Subgroup.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 (Subgroup.comap φ M)

@[instance 75]

instance AddSubgroupClass.toOrderedAddCommGroup {G : Type u_1} {S : Type u_2} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) : OrderedAddCommGroup ↥H

An additive subgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

Equations

• AddSubgroupClass.toOrderedAddCommGroup H = Function.Injective.orderedAddCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance SubgroupClass.toOrderedCommGroup {G : Type u_1} {S : Type u_2} [SetLike S G] [OrderedCommGroup G] [SubgroupClass S G] (H : S) : OrderedCommGroup ↥H

A subgroup of an OrderedCommGroup is an OrderedCommGroup.

Equations

• SubgroupClass.toOrderedCommGroup H = Function.Injective.orderedCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance AddSubgroupClass.toLinearOrderedAddCommGroup {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) : LinearOrderedAddCommGroup ↥H

An additive subgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

Equations

• AddSubgroupClass.toLinearOrderedAddCommGroup H = Function.Injective.linearOrderedAddCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance SubgroupClass.toLinearOrderedCommGroup {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedCommGroup G] [SubgroupClass S G] (H : S) : LinearOrderedCommGroup ↥H

A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

Equations

• SubgroupClass.toLinearOrderedCommGroup H = Function.Injective.linearOrderedCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AddSubgroup.toOrderedAddCommGroup {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) : OrderedAddCommGroup ↥H

An AddSubgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

Equations

• H.toOrderedAddCommGroup = Function.Injective.orderedAddCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Subgroup.toOrderedCommGroup {G : Type u_1} [OrderedCommGroup G] (H : Subgroup G) : OrderedCommGroup ↥H

A subgroup of an OrderedCommGroup is an OrderedCommGroup.

Equations

• H.toOrderedCommGroup = Function.Injective.orderedCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AddSubgroup.toLinearOrderedAddCommGroup {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) : LinearOrderedAddCommGroup ↥H

An AddSubgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

Equations

• H.toLinearOrderedAddCommGroup = Function.Injective.linearOrderedAddCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Subgroup.toLinearOrderedCommGroup {G : Type u_1} [LinearOrderedCommGroup G] (H : Subgroup G) : LinearOrderedCommGroup ↥H

A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

Equations

• H.toLinearOrderedCommGroup = Function.Injective.linearOrderedCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

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

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

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

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