Ordered instances on subgroups #

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

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

ZeroMemClass S G

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

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

NegMemClass S G

source

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

AddSubmonoidClass S G

source

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

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

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_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_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_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_3 {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] :

AddSubmonoidClass S G

source

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

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

NegMemClass 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_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_1 {G : Type u_1} {S : Type u_2} [SetLike S G] [LinearOrderedAddCommGroup G] [AddSubgroupClass S G] :

ZeroMemClass S G

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

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_2 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :

↑0 = ↑0

source

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

∀ (x : ↥H), ↑(-x) = ↑(-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_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_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_6 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) :

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

source

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

OrderedAddCommGroup ↥H

An AddSubgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

Equations

AddSubgroup.toOrderedAddCommGroup H = Function.Injective.orderedAddCommGroup (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 Subgroup.toOrderedCommGroup {G : Type u_1} [OrderedCommGroup G] (H : Subgroup G) :

OrderedCommGroup ↥H

A subgroup of an OrderedCommGroup is an OrderedCommGroup.

Equations

Subgroup.toOrderedCommGroup H = 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_4 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

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

source

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

↑0 = ↑0

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

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_7 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) :

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

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

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

LinearOrderedAddCommGroup ↥H

An AddSubgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

Equations

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

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

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

LinearOrderedCommGroup ↥H

A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

Equations

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

Documentation

Mathlib.GroupTheory.Subgroup.Order

Ordered instances on subgroups #