Facts about ordered structures and ordered instances on subgroups #

source

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

source

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

source

instance instIsModularLatticeAddSubgroup {C : Type u_1} [AddCommGroup C] :

IsModularLattice (AddSubgroup C)

Equations

⋯ = ⋯

source

instance instIsModularLatticeSubgroup {C : Type u_1} [CommGroup C] :

IsModularLattice (Subgroup C)

Equations

⋯ = ⋯

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

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

source

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

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

source

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_1 {G : Type u_2} {S : Type u_1} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] :

ZeroMemClass S G

source

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

source

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)

source

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)

source

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

source

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_2 {G : Type u_2} {S : Type u_1} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] :

NegMemClass S G

source

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)

source

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_3 {G : Type u_2} {S : Type u_1} [SetLike S G] [OrderedAddCommGroup G] [AddSubgroupClass S G] :

AddSubmonoidClass S G

source

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_4 {G : Type u_1} {S : Type u_2} [SetLike S G] (H : S) :

Function.Injective fun (a : ↥H) => ↑a

source

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)

source

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)

source

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

source

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

↑0 = ↑0

source

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)

source

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_1 {G : Type u_2} {S : Type u_1} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] :

ZeroMemClass S G

source

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)

source

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)

source

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)

source

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

source

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)

source

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_2 {G : Type u_2} {S : Type u_1} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] :

NegMemClass S G

source

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)

source

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_3 {G : Type u_2} {S : Type u_1} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] :

AddSubmonoidClass S G

source

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_4 {G : Type u_1} {S : Type u_2} [SetLike S G] (H : S) :

Function.Injective fun (a : ↥H) => ↑a

source

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)

source

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

source

theorem AddSubgroup.toOrderedAddCommGroup.proof_1 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :

Function.Injective fun (a : ↥H) => ↑a

source

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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

theorem AddSubgroup.toOrderedAddCommGroup.proof_6 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x : ↥H) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

source

theorem AddSubgroup.toOrderedAddCommGroup.proof_5 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x x_1 : ↥H), ↑(x - x_1) = ↑(x - x_1)

source

theorem AddSubgroup.toOrderedAddCommGroup.proof_4 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x : ↥H), ↑(-x) = ↑(-x)

source

theorem AddSubgroup.toOrderedAddCommGroup.proof_3 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x x_1 : ↥H), ↑(x + x_1) = ↑(x + x_1)

source

theorem AddSubgroup.toOrderedAddCommGroup.proof_7 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x : ↥H) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

source

theorem AddSubgroup.toOrderedAddCommGroup.proof_2 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :

↑0 = ↑0

source

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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_5 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x x_1 : ↥H), ↑(x - x_1) = ↑(x - x_1)

source

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_2 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

↑0 = ↑0

source

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_9 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x x_1 : ↥H), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

source

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_3 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x x_1 : ↥H), ↑(x + x_1) = ↑(x + x_1)

source

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_4 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x : ↥H), ↑(-x) = ↑(-x)

source

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_6 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x : ↥H) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

source

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_1 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

Function.Injective fun (a : ↥H) => ↑a

source

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_8 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x x_1 : ↥H), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

source

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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_7 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

∀ (x : ↥H) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

source

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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

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

StrictMono ⇑AddSubsemigroup.topEquiv

source

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

StrictMono ⇑Subsemigroup.topEquiv

source

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

StrictMono ⇑(AddEquiv.subsemigroupCongr h)

source

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

StrictMono ⇑(MulEquiv.subsemigroupCongr h)

source

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

source

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

HepLean Documentation

Mathlib.Algebra.Group.Subgroup.Order

Facts about ordered structures and ordered instances on subgroups #