Documentation

Mathlib.Algebra.Group.Subgroup.Order

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
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} :
@[simp]
theorem Subgroup.isCoatom_map {G : Type u_1} [Group G] (H : Subgroup G) (f : G ≃* H) {K : Subgroup G} :
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) :
theorem AddSubgroupClass.toOrderedAddCommGroup.proof_5 {G : Type u_1} {S : Type u_2} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
0 = 0
theorem AddSubgroupClass.toOrderedAddCommGroup.proof_7 {G : Type u_1} {S : Type u_2} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x : H), (-x) = (-x)
theorem AddSubgroupClass.toOrderedAddCommGroup.proof_10 {G : Type u_1} {S : Type u_2} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
@[instance 75]

An additive subgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

Equations
theorem AddSubgroupClass.toOrderedAddCommGroup.proof_8 {G : Type u_1} {S : Type u_2} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x x_1 : H), (x - x_1) = (x - x_1)
theorem AddSubgroupClass.toOrderedAddCommGroup.proof_4 {G : Type u_1} {S : Type u_2} [SetLike S G] (H : S) :
Function.Injective fun (a : H) => a
theorem AddSubgroupClass.toOrderedAddCommGroup.proof_9 {G : Type u_1} {S : Type u_2} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubgroupClass.toOrderedAddCommGroup.proof_6 {G : Type u_1} {S : Type u_2} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x x_1 : H), (x + x_1) = (x + x_1)
@[instance 75]
instance SubgroupClass.toOrderedCommGroup {G : Type u_1} {S : Type u_2} [SetLike S G] [OrderedCommGroup G] [SubgroupClass S G] (H : S) :

A subgroup of an OrderedCommGroup is an OrderedCommGroup.

Equations
theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_10 {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_12 {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] (H : S) :
∀ (x x_1 : H), (x x_1) = (x x_1)
theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_9 {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_11 {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] (H : S) :
∀ (x x_1 : H), (x x_1) = (x x_1)
@[instance 75]

An additive subgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

Equations
theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_6 {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x x_1 : H), (x + x_1) = (x + x_1)
theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_7 {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x : H), (-x) = (-x)
theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_4 {G : Type u_1} {S : Type u_2} [SetLike S G] (H : S) :
Function.Injective fun (a : H) => a
theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_8 {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] (H : S) :
∀ (x x_1 : H), (x - x_1) = (x - x_1)
@[instance 75]

A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

Equations

An AddSubgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

Equations
theorem AddSubgroup.toOrderedAddCommGroup.proof_6 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubgroup.toOrderedAddCommGroup.proof_5 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x x_1 : H), (x - x_1) = (x - x_1)
theorem AddSubgroup.toOrderedAddCommGroup.proof_4 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x : H), (-x) = (-x)
theorem AddSubgroup.toOrderedAddCommGroup.proof_3 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x x_1 : H), (x + x_1) = (x + x_1)
theorem AddSubgroup.toOrderedAddCommGroup.proof_7 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)

A subgroup of an OrderedCommGroup is an OrderedCommGroup.

Equations
theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_5 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x x_1 : H), (x - x_1) = (x - x_1)
theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_9 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x x_1 : H), (x x_1) = (x x_1)
theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_3 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x x_1 : H), (x + x_1) = (x + x_1)
theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_4 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x : H), (-x) = (-x)
theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_6 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_8 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x x_1 : H), (x x_1) = (x x_1)

An AddSubgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

Equations
theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_7 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :
∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)

A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

Equations
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_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