Groups

This file defines additive and multiplicative group structures. Division monoid structures are defined in Mathlib.Algebra.Group.DivInvMonoid.

class Group (G : Type u_2) extends DivInvMonoid G : Type u_2

A Group is a Monoid with an operation ⁻¹ satisfying a⁻¹ * a = 1.

There is also a division operation / such that a / b = a * b⁻¹, with a default so that a / b = a * b⁻¹ holds by definition.

Use Group.ofLeftAxioms or Group.ofRightAxioms to define a group structure on a type with the minimum proof obligations.

Wikidata Q83478

• one : G
• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• one_mul (a : G) : 1 * a = a
• mul_one (a : G) : a * 1 = a
• npow : ℕ → G → G
• npow_zero (x : G) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : G) : x ^ (n + 1) = x ^ n * x
• inv : G → G
• div : G → G → G
• zpow : ℤ → G → G
• div_eq_mul_inv (a b : G) : a / b = a * b⁻¹
• zpow_zero' (a : G) : a ^ 0 = 1
• zpow_succ' (n : ℕ) (a : G) : a ^ ↑n.succ = a ^ ↑n * a
• zpow_neg' (n : ℕ) (a : G) : a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
• inv_mul_cancel (a : G) : a⁻¹ * a = 1

class AddGroup (A : Type u_2) extends SubNegMonoid A : Type u_2

An AddGroup is an AddMonoid with a unary - satisfying -a + a = 0.

There is also a binary operation - such that a - b = a + -b, with a default so that a - b = a + -b holds by definition.

Use AddGroup.ofLeftAxioms or AddGroup.ofRightAxioms to define an additive group structure on a type with the minimum proof obligations.

Wikidata Q83478

• zero : A
• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : A) : (n + 1) • x = n • x + x
• neg : A → A
• sub : A → A → A
• zsmul : ℤ → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul_zero' (a : A) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : A) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : A) : Int.negSucc n • a = -(↑n.succ • a)
• neg_add_cancel (a : A) : -a + a = 0

@[simp]

theorem inv_mul_cancel {G : Type u_1} [Group G] (a : G) : a⁻¹ * a = 1

@[simp]

theorem neg_add_cancel {G : Type u_1} [AddGroup G] (a : G) : -a + a = 0

@[simp]

theorem mul_inv_cancel {G : Type u_1} [Group G] (a : G) : a * a⁻¹ = 1

@[simp]

theorem add_neg_cancel {G : Type u_1} [AddGroup G] (a : G) : a + -a = 0

@[simp]

theorem div_self' {G : Type u_1} [Group G] (a : G) : a / a = 1

@[simp]

theorem sub_self {G : Type u_1} [AddGroup G] (a : G) : a - a = 0

@[simp]

theorem inv_mul_cancel_left {G : Type u_1} [Group G] (a b : G) : a⁻¹ * (a * b) = b

@[simp]

theorem neg_add_cancel_left {G : Type u_1} [AddGroup G] (a b : G) : -a + (a + b) = b

@[simp]

theorem mul_inv_cancel_left {G : Type u_1} [Group G] (a b : G) : a * (a⁻¹ * b) = b

@[simp]

theorem add_neg_cancel_left {G : Type u_1} [AddGroup G] (a b : G) : a + (-a + b) = b

@[simp]

theorem mul_inv_cancel_right {G : Type u_1} [Group G] (a b : G) : a * b * b⁻¹ = a

@[simp]

theorem add_neg_cancel_right {G : Type u_1} [AddGroup G] (a b : G) : a + b + -b = a

@[simp]

theorem mul_div_cancel_right {G : Type u_1} [Group G] (a b : G) : a * b / b = a

@[simp]

theorem add_sub_cancel_right {G : Type u_1} [AddGroup G] (a b : G) : a + b - b = a

@[simp]

theorem inv_mul_cancel_right {G : Type u_1} [Group G] (a b : G) : a * b⁻¹ * b = a

@[simp]

theorem neg_add_cancel_right {G : Type u_1} [AddGroup G] (a b : G) : a + -b + b = a

@[simp]

theorem div_mul_cancel {G : Type u_1} [Group G] (a b : G) : a / b * b = a

@[simp]

theorem sub_add_cancel {G : Type u_1} [AddGroup G] (a b : G) : a - b + b = a

@[instance_reducible, instance 100]

instance Group.toDivisionMonoid {G : Type u_1} [Group G] : DivisionMonoid G

@[instance_reducible, instance 100]

instance AddGroup.toSubtractionMonoid {G : Type u_1} [AddGroup G] : SubtractionMonoid G

@[instance_reducible, instance 100]

instance Group.toCancelMonoid {G : Type u_1} [Group G] : CancelMonoid G

@[instance_reducible, instance 100]

instance AddGroup.toAddCancelMonoid {G : Type u_1} [AddGroup G] : AddCancelMonoid G

class AddCommGroup (G : Type u_2) extends AddGroup G, AddCommMonoid G : Type u_2

An additive commutative group is an additive group with commutative (+).

Wikidata Q181296

• zero : G
• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• zero_add (a : G) : 0 + a = a
• add_zero (a : G) : a + 0 = a
• nsmul : ℕ → G → G
• nsmul_zero (x : G) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : G) : (n + 1) • x = n • x + x
• neg : G → G
• sub : G → G → G
• zsmul : ℤ → G → G
• sub_eq_add_neg (a b : G) : a - b = a + -b
• zsmul_zero' (a : G) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : G) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : G) : Int.negSucc n • a = -(↑n.succ • a)
• neg_add_cancel (a : G) : -a + a = 0
• add_comm (a b : G) : a + b = b + a

class CommGroup (G : Type u_2) extends Group G, CommMonoid G : Type u_2

A commutative group is a group with commutative (*).

Wikidata Q181296

• one : G
• mul : G → G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• one_mul (a : G) : 1 * a = a
• mul_one (a : G) : a * 1 = a
• npow : ℕ → G → G
• npow_zero (x : G) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : G) : x ^ (n + 1) = x ^ n * x
• inv : G → G
• div : G → G → G
• zpow : ℤ → G → G
• div_eq_mul_inv (a b : G) : a / b = a * b⁻¹
• zpow_zero' (a : G) : a ^ 0 = 1
• zpow_succ' (n : ℕ) (a : G) : a ^ ↑n.succ = a ^ ↑n * a
• zpow_neg' (n : ℕ) (a : G) : a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
• inv_mul_cancel (a : G) : a⁻¹ * a = 1
• mul_comm (a b : G) : a * b = b * a

@[instance_reducible, instance 100]

instance CommGroup.toCancelCommMonoid {G : Type u_1} [CommGroup G] : CancelCommMonoid G

@[instance_reducible, instance 100]

instance AddCommGroup.toAddCancelCommMonoid {G : Type u_1} [AddCommGroup G] : AddCancelCommMonoid G

@[instance_reducible, instance 100]

instance CommGroup.toDivisionCommMonoid {G : Type u_1} [CommGroup G] : DivisionCommMonoid G

@[instance_reducible, instance 100]

instance AddCommGroup.toDivisionAddCommMonoid {G : Type u_1} [AddCommGroup G] : SubtractionCommMonoid G

@[simp]

theorem inv_mul_cancel_comm {G : Type u_1} [CommGroup G] (a b : G) : a⁻¹ * b * a = b

@[simp]

theorem neg_add_cancel_comm {G : Type u_1} [AddCommGroup G] (a b : G) : -a + b + a = b

@[simp]

theorem mul_inv_cancel_comm {G : Type u_1} [CommGroup G] (a b : G) : a * b * a⁻¹ = b

@[simp]

theorem add_neg_cancel_comm {G : Type u_1} [AddCommGroup G] (a b : G) : a + b + -a = b

@[simp]

theorem inv_mul_cancel_comm_assoc {G : Type u_1} [CommGroup G] (a b : G) : a⁻¹ * (b * a) = b

@[simp]

theorem neg_add_cancel_comm_assoc {G : Type u_1} [AddCommGroup G] (a b : G) : -a + (b + a) = b

@[simp]

theorem mul_inv_cancel_comm_assoc {G : Type u_1} [CommGroup G] (a b : G) : a * (b * a⁻¹) = b

@[simp]

theorem add_neg_cancel_comm_assoc {G : Type u_1} [AddCommGroup G] (a b : G) : a + (b + -a) = b

We initialize the projections for the group structures for @[simps] here.

The lemmas generated for the npow/zpow projections will not apply to x ^ y, since the argument order of these projections does not match the argument order of ^. The nsmul/zsmul lemmas are correct.