Typeclasses for (semi)groups and monoids

In this file we define typeclasses for algebraic structures with one binary operation. The classes are named (Add)?(Comm)?(Semigroup|Monoid|Group), where Add means that the class uses additive notation and Comm means that the class assumes that the binary operation is commutative.

The file does not contain any lemmas except for

• axioms of typeclasses restated in the root namespace;
• lemmas required for instances.

For basic lemmas about these classes see Algebra.Group.Basic.

We also introduce notation classes SMul and VAdd for multiplicative and additive actions and register the following instances:

• Pow M ℕ, for monoids M, and Pow G ℤ for groups G;
• SMul ℕ M for additive monoids M, and SMul ℤ G for additive groups G.

Notation

• +, -, *, /, ^ : the usual arithmetic operations; the underlying functions are Add.add, Neg.neg/Sub.sub, Mul.mul, Div.div, and HPow.hPow.
• a • b is used as notation for HSMul.hSMul a b.
• a +ᵥ b is used as notation for HVAdd.hVAdd a b.

class HVAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) : Type (max (max u v) w)

• hVAdd : α → β → γ

  a +ᵥ b computes the sum of a and b. The meaning of this notation is type-dependent.

The notation typeclass for heterogeneous additive actions. This enables the notation a +ᵥ b : γ where a : α, b : β.

class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) : Type (max (max u v) w)

• hSMul : α → β → γ

  a • b computes the product of a and b. The meaning of this notation is type-dependent.

The notation typeclass for heterogeneous scalar multiplication. This enables the notation a • b : γ where a : α, b : β.

class VAdd (G : Type u_1) (P : Type u_2) : Type (max u_1 u_2)

• vadd : G → P → P

Type class for the +ᵥ notation.

class VSub (G : outParam (Type u_1)) (P : Type u_2) : Type (max u_1 u_2)

• vsub : P → P → G

Type class for the -ᵥ notation.

theorem VAdd.ext {G : Type u_1} {P : Type u_2} (x : VAdd G P) (y : VAdd G P) (vadd : VAdd.vadd = VAdd.vadd) : x = y

theorem SMul.ext_iff {M : Type u_1} {α : Type u_2} (x : SMul M α) (y : SMul M α) : x = y ↔ SMul.smul = SMul.smul

theorem VAdd.ext_iff {G : Type u_1} {P : Type u_2} (x : VAdd G P) (y : VAdd G P) : x = y ↔ VAdd.vadd = VAdd.vadd

theorem SMul.ext {M : Type u_1} {α : Type u_2} (x : SMul M α) (y : SMul M α) (smul : SMul.smul = SMul.smul) : x = y

class SMul (M : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

• smul : M → α → α

Typeclass for types with a scalar multiplication operation, denoted • (\bu)

def «term_+ᵥ_» : Lean.TrailingParserDescr

Equations

• «term_+ᵥ_» = Lean.ParserDescr.trailingNode `term_+ᵥ_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +ᵥ ") (Lean.ParserDescr.cat `term 66))

def «term_-ᵥ_» : Lean.TrailingParserDescr

Equations

• «term_-ᵥ_» = Lean.ParserDescr.trailingNode `term_-ᵥ_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -ᵥ ") (Lean.ParserDescr.cat `term 66))

def «term_•_» : Lean.TrailingParserDescr

Equations

• «term_•_» = Lean.ParserDescr.trailingNode `term_•_ 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " • ") (Lean.ParserDescr.cat `term 73))

@[defaultInstance 1000]

instance instHVAdd {α : Type u_1} {β : Type u_2} [VAdd α β] : HVAdd α β β

Equations

• instHVAdd = { hVAdd := VAdd.vadd }

@[defaultInstance 1000]

instance instHSMul {α : Type u_1} {β : Type u_2} [SMul α β] : HSMul α β β

Equations

• instHSMul = { hSMul := SMul.smul }

class Inv (α : Type u) : Type u

• inv : α → α

  Invert an element of α.

Class of types that have an inversion operation.

def «term_⁻¹» : Lean.TrailingParserDescr

Invert an element of α.

Equations

• «term_⁻¹» = Lean.ParserDescr.trailingNode `term_⁻¹ 1024 1024 (Lean.ParserDescr.symbol "⁻¹")

def leftAdd {G : Type u_1} [Add G] : G → G → G

leftAdd g denotes left addition by g

Equations

• leftAdd g x = g + x

def leftMul {G : Type u_1} [Mul G] : G → G → G

leftMul g denotes left multiplication by g

Equations

• leftMul g x = g * x

def rightAdd {G : Type u_1} [Add G] : G → G → G

rightAdd g denotes right addition by g

Equations

• rightAdd g x = x + g

def rightMul {G : Type u_1} [Mul G] : G → G → G

rightMul g denotes right multiplication by g

Equations

• rightMul g x = x * g

class IsLeftCancelMul (G : Type u) [Mul G] : Prop

• mul_left_cancel : ∀ (a b c : G), a * b = a * c → b = c

  Multiplication is left cancellative.

A mixin for left cancellative multiplication.

class IsRightCancelMul (G : Type u) [Mul G] : Prop

• mul_right_cancel : ∀ (a b c : G), a * b = c * b → a = c

  Multiplication is right cancellative.

A mixin for right cancellative multiplication.

class IsCancelMul (G : Type u) [Mul G] extends IsLeftCancelMul , IsRightCancelMul : Prop

A mixin for cancellative multiplication.

class IsLeftCancelAdd (G : Type u) [Add G] : Prop

• add_left_cancel : ∀ (a b c : G), a + b = a + c → b = c

  Addition is left cancellative.

A mixin for left cancellative addition.

class IsRightCancelAdd (G : Type u) [Add G] : Prop

• add_right_cancel : ∀ (a b c : G), a + b = c + b → a = c

  Addition is right cancellative.

A mixin for right cancellative addition.

class IsCancelAdd (G : Type u) [Add G] extends IsLeftCancelAdd , IsRightCancelAdd : Prop

A mixin for cancellative addition.

theorem add_left_cancel {G : Type u_1} [Add G] [IsLeftCancelAdd G] {a : G} {b : G} {c : G} : a + b = a + c → b = c

theorem mul_left_cancel {G : Type u_1} [Mul G] [IsLeftCancelMul G] {a : G} {b : G} {c : G} : a * b = a * c → b = c

theorem add_left_cancel_iff {G : Type u_1} [Add G] [IsLeftCancelAdd G] {a : G} {b : G} {c : G} : a + b = a + c ↔ b = c

theorem mul_left_cancel_iff {G : Type u_1} [Mul G] [IsLeftCancelMul G] {a : G} {b : G} {c : G} : a * b = a * c ↔ b = c

theorem add_right_injective {G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) : Function.Injective ((fun x x_1 => x + x_1) a)

theorem mul_right_injective {G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) : Function.Injective ((fun x x_1 => x * x_1) a)

@[simp]

theorem add_right_inj {G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) {b : G} {c : G} : a + b = a + c ↔ b = c

@[simp]

theorem mul_right_inj {G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) {b : G} {c : G} : a * b = a * c ↔ b = c

theorem add_ne_add_right {G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) {b : G} {c : G} : a + b ≠ a + c ↔ b ≠ c

theorem mul_ne_mul_right {G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) {b : G} {c : G} : a * b ≠ a * c ↔ b ≠ c

theorem add_right_cancel {G : Type u_1} [Add G] [IsRightCancelAdd G] {a : G} {b : G} {c : G} : a + b = c + b → a = c

theorem mul_right_cancel {G : Type u_1} [Mul G] [IsRightCancelMul G] {a : G} {b : G} {c : G} : a * b = c * b → a = c

theorem add_right_cancel_iff {G : Type u_1} [Add G] [IsRightCancelAdd G] {a : G} {b : G} {c : G} : b + a = c + a ↔ b = c

theorem mul_right_cancel_iff {G : Type u_1} [Mul G] [IsRightCancelMul G] {a : G} {b : G} {c : G} : b * a = c * a ↔ b = c

theorem add_left_injective {G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) : Function.Injective fun x => x + a

theorem mul_left_injective {G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) : Function.Injective fun x => x * a

@[simp]

theorem add_left_inj {G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) {b : G} {c : G} : b + a = c + a ↔ b = c

@[simp]

theorem mul_left_inj {G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) {b : G} {c : G} : b * a = c * a ↔ b = c

theorem add_ne_add_left {G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) {b : G} {c : G} : b + a ≠ c + a ↔ b ≠ c

theorem mul_ne_mul_left {G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) {b : G} {c : G} : b * a ≠ c * a ↔ b ≠ c

theorem Semigroup.ext {G : Type u} (x : Semigroup G) (y : Semigroup G) (mul : Mul.mul = Mul.mul) : x = y

theorem Semigroup.ext_iff {G : Type u} (x : Semigroup G) (y : Semigroup G) : x = y ↔ Mul.mul = Mul.mul

class Semigroup (G : Type u) extends Mul : Type u

• mul : G → G → G
• mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)

  Multiplication is associative

A semigroup is a type with an associative (*).

theorem AddSemigroup.ext {G : Type u} (x : AddSemigroup G) (y : AddSemigroup G) (add : Add.add = Add.add) : x = y

theorem AddSemigroup.ext_iff {G : Type u} (x : AddSemigroup G) (y : AddSemigroup G) : x = y ↔ Add.add = Add.add

class AddSemigroup (G : Type u) extends Add : Type u

• add : G → G → G
• add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)

  Addition is associative

An additive semigroup is a type with an associative (+).

theorem add_assoc {G : Type u_1} [AddSemigroup G] (a : G) (b : G) (c : G) : a + b + c = a + (b + c)

theorem mul_assoc {G : Type u_1} [Semigroup G] (a : G) (b : G) (c : G) : a * b * c = a * (b * c)

theorem AddSemigroup.to_isAssociative.proof_1 {G : Type u_1} [AddSemigroup G] : IsAssociative G fun x x_1 => x + x_1

instance AddSemigroup.to_isAssociative {G : Type u_1} [AddSemigroup G] : IsAssociative G fun x x_1 => x + x_1

Equations

• @AddSemigroup.to_isAssociative = @AddSemigroup.to_isAssociative.proof_1

instance Semigroup.to_isAssociative {G : Type u_1} [Semigroup G] : IsAssociative G fun x x_1 => x * x_1

Equations

• @Semigroup.to_isAssociative = @Semigroup.to_isAssociative.proof_1

theorem CommSemigroup.ext {G : Type u} (x : CommSemigroup G) (y : CommSemigroup G) (mul : Mul.mul = Mul.mul) : x = y

theorem CommSemigroup.ext_iff {G : Type u} (x : CommSemigroup G) (y : CommSemigroup G) : x = y ↔ Mul.mul = Mul.mul

class CommSemigroup (G : Type u) extends Semigroup : Type u

• mul : G → G → G
• mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
• mul_comm : ∀ (a b : G), a * b = b * a

  Multiplication is commutative in a commutative semigroup.

A commutative semigroup is a type with an associative commutative (*).

theorem AddCommSemigroup.ext {G : Type u} (x : AddCommSemigroup G) (y : AddCommSemigroup G) (add : Add.add = Add.add) : x = y

theorem AddCommSemigroup.ext_iff {G : Type u} (x : AddCommSemigroup G) (y : AddCommSemigroup G) : x = y ↔ Add.add = Add.add

class AddCommSemigroup (G : Type u) extends AddSemigroup : Type u

• add : G → G → G
• add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
• add_comm : ∀ (a b : G), a + b = b + a

  Addition is commutative in an additive commutative semigroup.

A commutative additive semigroup is a type with an associative commutative (+).

theorem add_comm {G : Type u_1} [AddCommSemigroup G] (a : G) (b : G) : a + b = b + a

theorem mul_comm {G : Type u_1} [CommSemigroup G] (a : G) (b : G) : a * b = b * a

theorem AddCommSemigroup.to_isCommutative.proof_1 {G : Type u_1} [AddCommSemigroup G] : IsCommutative G fun x x_1 => x + x_1

instance AddCommSemigroup.to_isCommutative {G : Type u_1} [AddCommSemigroup G] : IsCommutative G fun x x_1 => x + x_1

Equations

• @AddCommSemigroup.to_isCommutative = @AddCommSemigroup.to_isCommutative.proof_1

instance CommSemigroup.to_isCommutative {G : Type u_1} [CommSemigroup G] : IsCommutative G fun x x_1 => x * x_1

Equations

• @CommSemigroup.to_isCommutative = @CommSemigroup.to_isCommutative.proof_1

theorem AddCommSemigroup.IsRightCancelAdd.toIsLeftCancelAdd (G : Type u) [AddCommSemigroup G] [IsRightCancelAdd G] : IsLeftCancelAdd G

Any AddCommSemigroup G that satisfies IsRightCancelAdd G also satisfies IsLeftCancelAdd G.

theorem CommSemigroup.IsRightCancelMul.toIsLeftCancelMul (G : Type u) [CommSemigroup G] [IsRightCancelMul G] : IsLeftCancelMul G

Any CommSemigroup G that satisfies IsRightCancelMul G also satisfies IsLeftCancelMul G.

theorem AddCommSemigroup.IsLeftCancelAdd.toIsRightCancelAdd (G : Type u) [AddCommSemigroup G] [IsLeftCancelAdd G] : IsRightCancelAdd G

Any AddCommSemigroup G that satisfies IsLeftCancelAdd G also satisfies IsRightCancelAdd G.

theorem CommSemigroup.IsLeftCancelMul.toIsRightCancelMul (G : Type u) [CommSemigroup G] [IsLeftCancelMul G] : IsRightCancelMul G

Any CommSemigroup G that satisfies IsLeftCancelMul G also satisfies IsRightCancelMul G.

theorem AddCommSemigroup.IsLeftCancelAdd.toIsCancelAdd (G : Type u) [AddCommSemigroup G] [IsLeftCancelAdd G] : IsCancelAdd G

Any AddCommSemigroup G that satisfies IsLeftCancelAdd G also satisfies IsCancelAdd G.

theorem CommSemigroup.IsLeftCancelMul.toIsCancelMul (G : Type u) [CommSemigroup G] [IsLeftCancelMul G] : IsCancelMul G

Any CommSemigroup G that satisfies IsLeftCancelMul G also satisfies IsCancelMul G.

theorem AddCommSemigroup.IsRightCancelAdd.toIsCancelAdd (G : Type u) [AddCommSemigroup G] [IsRightCancelAdd G] : IsCancelAdd G

Any AddCommSemigroup G that satisfies IsRightCancelAdd G also satisfies IsCancelAdd G.

theorem CommSemigroup.IsRightCancelMul.toIsCancelMul (G : Type u) [CommSemigroup G] [IsRightCancelMul G] : IsCancelMul G

Any CommSemigroup G that satisfies IsRightCancelMul G also satisfies IsCancelMul G.

theorem LeftCancelSemigroup.ext {G : Type u} (x : LeftCancelSemigroup G) (y : LeftCancelSemigroup G) (mul : Mul.mul = Mul.mul) : x = y

theorem LeftCancelSemigroup.ext_iff {G : Type u} (x : LeftCancelSemigroup G) (y : LeftCancelSemigroup G) : x = y ↔ Mul.mul = Mul.mul

class LeftCancelSemigroup (G : Type u) extends Semigroup : Type u

• mul : G → G → G
• mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
• mul_left_cancel : ∀ (a b c : G), a * b = a * c → b = c

A LeftCancelSemigroup is a semigroup such that a * b = a * c implies b = c.

theorem AddLeftCancelSemigroup.ext {G : Type u} (x : AddLeftCancelSemigroup G) (y : AddLeftCancelSemigroup G) (add : Add.add = Add.add) : x = y

theorem AddLeftCancelSemigroup.ext_iff {G : Type u} (x : AddLeftCancelSemigroup G) (y : AddLeftCancelSemigroup G) : x = y ↔ Add.add = Add.add

class AddLeftCancelSemigroup (G : Type u) extends AddSemigroup : Type u

• add : G → G → G
• add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
• add_left_cancel : ∀ (a b c : G), a + b = a + c → b = c

An AddLeftCancelSemigroup is an additive semigroup such that a + b = a + c implies b = c.

instance AddLeftCancelSemigroup.toIsLeftCancelAdd (G : Type u) [AddLeftCancelSemigroup G] : IsLeftCancelAdd G

Any AddLeftCancelSemigroup satisfies IsLeftCancelAdd.

Equations

• AddLeftCancelSemigroup.toIsLeftCancelAdd = AddLeftCancelSemigroup.toIsLeftCancelAdd.proof_1

theorem AddLeftCancelSemigroup.toIsLeftCancelAdd.proof_1 (G : Type u_1) [AddLeftCancelSemigroup G] : IsLeftCancelAdd G

instance LeftCancelSemigroup.toIsLeftCancelMul (G : Type u) [LeftCancelSemigroup G] : IsLeftCancelMul G

Any LeftCancelSemigroup satisfies IsLeftCancelMul.

Equations

• LeftCancelSemigroup.toIsLeftCancelMul = LeftCancelSemigroup.toIsLeftCancelMul.proof_1

theorem RightCancelSemigroup.ext {G : Type u} (x : RightCancelSemigroup G) (y : RightCancelSemigroup G) (mul : Mul.mul = Mul.mul) : x = y

theorem RightCancelSemigroup.ext_iff {G : Type u} (x : RightCancelSemigroup G) (y : RightCancelSemigroup G) : x = y ↔ Mul.mul = Mul.mul

class RightCancelSemigroup (G : Type u) extends Semigroup : Type u

• mul : G → G → G
• mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
• mul_right_cancel : ∀ (a b c : G), a * b = c * b → a = c

A RightCancelSemigroup is a semigroup such that a * b = c * b implies a = c.

theorem AddRightCancelSemigroup.ext {G : Type u} (x : AddRightCancelSemigroup G) (y : AddRightCancelSemigroup G) (add : Add.add = Add.add) : x = y

theorem AddRightCancelSemigroup.ext_iff {G : Type u} (x : AddRightCancelSemigroup G) (y : AddRightCancelSemigroup G) : x = y ↔ Add.add = Add.add

class AddRightCancelSemigroup (G : Type u) extends AddSemigroup : Type u

• add : G → G → G
• add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
• add_right_cancel : ∀ (a b c : G), a + b = c + b → a = c

An AddRightCancelSemigroup is an additive semigroup such that a + b = c + b implies a = c.

instance AddRightCancelSemigroup.toIsRightCancelAdd (G : Type u) [AddRightCancelSemigroup G] : IsRightCancelAdd G

Any AddRightCancelSemigroup satisfies IsRightCancelAdd.

Equations

• AddRightCancelSemigroup.toIsRightCancelAdd = AddRightCancelSemigroup.toIsRightCancelAdd.proof_1

theorem AddRightCancelSemigroup.toIsRightCancelAdd.proof_1 (G : Type u_1) [AddRightCancelSemigroup G] : IsRightCancelAdd G

instance RightCancelSemigroup.toIsRightCancelMul (G : Type u) [RightCancelSemigroup G] : IsRightCancelMul G

Any RightCancelSemigroup satisfies IsRightCancelMul.

Equations

• RightCancelSemigroup.toIsRightCancelMul = RightCancelSemigroup.toIsRightCancelMul.proof_1

class MulOneClass (M : Type u) extends One , Mul : Type u

• one : M
• mul : M → M → M
• one_mul : ∀ (a : M), 1 * a = a

  One is a left neutral element for multiplication

• mul_one : ∀ (a : M), a * 1 = a

  One is a right neutral element for multiplication

Typeclass for expressing that a type M with multiplication and a one satisfies 1 * a = a and a * 1 = a for all a : M.

class AddZeroClass (M : Type u) extends Zero , Add : Type u

• zero : M
• add : M → M → M
• zero_add : ∀ (a : M), 0 + a = a

  Zero is a left neutral element for addition

• add_zero : ∀ (a : M), a + 0 = a

  Zero is a right neutral element for addition

Typeclass for expressing that a type M with addition and a zero satisfies 0 + a = a and a + 0 = a for all a : M.

theorem AddZeroClass.ext {M : Type u} ⦃m₁ : AddZeroClass M⦄ ⦃m₂ : AddZeroClass M⦄ : Add.add = Add.add → m₁ = m₂

theorem MulOneClass.ext {M : Type u} ⦃m₁ : MulOneClass M⦄ ⦃m₂ : MulOneClass M⦄ : Mul.mul = Mul.mul → m₁ = m₂

@[simp]

theorem zero_add {M : Type u} [AddZeroClass M] (a : M) : 0 + a = a

@[simp]

theorem one_mul {M : Type u} [MulOneClass M] (a : M) : 1 * a = a

@[simp]

theorem add_zero {M : Type u} [AddZeroClass M] (a : M) : a + 0 = a

@[simp]

theorem mul_one {M : Type u} [MulOneClass M] (a : M) : a * 1 = a

def npowRec {M : Type u} [One M] [Mul M] : ℕ → M → M

The fundamental power operation in a monoid. npowRec n a = a*a*...*a n times. Use instead a ^ n, which has better definitional behavior.

Equations

• npowRec 0 x = 1
• npowRec (Nat.succ n) x = x * npowRec n x

def nsmulRec {M : Type u} [Zero M] [Add M] : ℕ → M → M

The fundamental scalar multiplication in an additive monoid. nsmulRec n a = a+a+...+a n times. Use instead n • a, which has better definitional behavior.

Equations

• nsmulRec 0 x = 0
• nsmulRec (Nat.succ n) x = x + nsmulRec n x

Design note on AddMonoid and Monoid

An AddMonoid has a natural ℕ-action, defined by n • a = a + ... + a, that we want to declare as an instance as it makes it possible to use the language of linear algebra. However, there are often other natural ℕ-actions. For instance, for any semiring R, the space of polynomials Polynomial R has a natural R-action defined by multiplication on the coefficients. This means that Polynomial ℕ would have two natural ℕ-actions, which are equal but not defeq. The same goes for linear maps, tensor products, and so on (and even for ℕ itself).

To solve this issue, we embed an ℕ-action in the definition of an AddMonoid (which is by default equal to the naive action a + ... + a, but can be adjusted when needed), and declare a SMul ℕ α instance using this action. See Note [forgetful inheritance] for more explanations on this pattern.

For example, when we define Polynomial R, then we declare the ℕ-action to be by multiplication on each coefficient (using the ℕ-action on R that comes from the fact that R is an AddMonoid). In this way, the two natural SMul ℕ (Polynomial ℕ) instances are defeq.

The tactic to_additive transfers definitions and results from multiplicative monoids to additive monoids. To work, it has to map fields to fields. This means that we should also add corresponding fields to the multiplicative structure Monoid, which could solve defeq problems for powers if needed. These problems do not come up in practice, so most of the time we will not need to adjust the npow field when defining multiplicative objects.

A basic theory for the power function on monoids and the ℕ-action on additive monoids is built in the file Algebra.GroupPower.Basic. For now, we only register the most basic properties that we need right away.

class AddMonoid (M : Type u) extends AddSemigroup , Zero : Type u

• add : M → M → M
• add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)
• zero : M
• zero_add : ∀ (a : M), 0 + a = a

  Zero is a left neutral element for addition

• add_zero : ∀ (a : M), a + 0 = a

  Zero is a right neutral element for addition

• nsmul : ℕ → M → M

  Multiplication by a natural number.

• nsmul_zero : ∀ (x : M), AddMonoid.nsmul 0 x = 0

  Multiplication by (0 : ℕ) gives 0.

• nsmul_succ : ∀ (n : ℕ) (x : M), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

  Multiplication by (n + 1 : ℕ) behaves as expected.

An AddMonoid is an AddSemigroup with an element 0 such that 0 + a = a + 0 = a.

class Monoid (M : Type u) extends Semigroup , One : Type u

• mul : M → M → M
• mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c)
• one : M
• one_mul : ∀ (a : M), 1 * a = a

  One is a left neutral element for multiplication

• mul_one : ∀ (a : M), a * 1 = a

  One is a right neutral element for multiplication

• npow : ℕ → M → M

  Raising to the power of a natural number.

• npow_zero : ∀ (x : M), Monoid.npow 0 x = 1

  Raising to the power (0 : ℕ) gives 1.

• npow_succ : ∀ (n : ℕ) (x : M), Monoid.npow (n + 1) x = x * Monoid.npow n x

  Raising to the power (n + 1 : ℕ) behaves as expected.

A Monoid is a Semigroup with an element 1 such that 1 * a = a * 1 = a.

@[defaultInstance 10000]

instance Monoid.Pow {M : Type u_2} [Monoid M] : Pow M ℕ

Equations

• Monoid.Pow = { pow := fun x n => Monoid.npow n x }

instance AddMonoid.SMul {M : Type u_2} [AddMonoid M] : SMul ℕ M

Equations

• AddMonoid.SMul = { smul := AddMonoid.nsmul }

@[simp]

theorem nsmul_eq_smul {M : Type u_2} [AddMonoid M] (n : ℕ) (x : M) : AddMonoid.nsmul n x = n • x

@[simp]

theorem npow_eq_pow {M : Type u_2} [Monoid M] (n : ℕ) (x : M) : Monoid.npow n x = x ^ n

theorem zero_nsmul {M : Type u_2} [AddMonoid M] (a : M) : 0 • a = 0

@[simp]

theorem pow_zero {M : Type u_2} [Monoid M] (a : M) : a ^ 0 = 1

theorem succ_nsmul {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) : (n + 1) • a = a + n • a

theorem pow_succ {M : Type u_2} [Monoid M] (a : M) (n : ℕ) : a ^ (n + 1) = a * a ^ n

theorem left_neg_eq_right_neg {M : Type u} [AddMonoid M] {a : M} {b : M} {c : M} (hba : b + a = 0) (hac : a + c = 0) : b = c

theorem left_inv_eq_right_inv {M : Type u} [Monoid M] {a : M} {b : M} {c : M} (hba : b * a = 1) (hac : a * c = 1) : b = c

class AddCommMonoid (M : Type u) extends AddMonoid : Type u

• add : M → M → M
• add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)
• zero : M
• zero_add : ∀ (a : M), 0 + a = a
• add_zero : ∀ (a : M), a + 0 = a
• nsmul : ℕ → M → M
• nsmul_zero : ∀ (x : M), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : M), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
• add_comm : ∀ (a b : M), a + b = b + a

  Addition is commutative in an additive commutative semigroup.

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

class CommMonoid (M : Type u) extends Monoid : Type u

• mul : M → M → M
• mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c)
• one : M
• one_mul : ∀ (a : M), 1 * a = a
• mul_one : ∀ (a : M), a * 1 = a
• npow : ℕ → M → M
• npow_zero : ∀ (x : M), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : M), Monoid.npow (n + 1) x = x * Monoid.npow n x
• mul_comm : ∀ (a b : M), a * b = b * a

  Multiplication is commutative in a commutative semigroup.

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

class AddLeftCancelMonoid (M : Type u) extends AddLeftCancelSemigroup , Zero : Type u

• add : M → M → M
• add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)
• add_left_cancel : ∀ (a b c : M), a + b = a + c → b = c
• zero : M
• zero_add : ∀ (a : M), 0 + a = a

  Zero is a left neutral element for addition

• add_zero : ∀ (a : M), a + 0 = a

  Zero is a right neutral element for addition

• nsmul : ℕ → M → M

  Multiplication by a natural number.

• nsmul_zero : ∀ (x : M), AddLeftCancelMonoid.nsmul 0 x = 0

  Multiplication by (0 : ℕ) gives 0.

• nsmul_succ : ∀ (n : ℕ) (x : M), AddLeftCancelMonoid.nsmul (n + 1) x = x + AddLeftCancelMonoid.nsmul n x

  Multiplication by (n + 1 : ℕ) behaves as expected.

An additive monoid in which addition is left-cancellative. Main examples are ℕ and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so AddLeftCancelSemigroup is not enough.

class LeftCancelMonoid (M : Type u) extends LeftCancelSemigroup , One : Type u

• mul : M → M → M
• mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c)
• mul_left_cancel : ∀ (a b c : M), a * b = a * c → b = c
• one : M
• one_mul : ∀ (a : M), 1 * a = a

  One is a left neutral element for multiplication

• mul_one : ∀ (a : M), a * 1 = a

  One is a right neutral element for multiplication

• npow : ℕ → M → M

  Raising to the power of a natural number.

• npow_zero : ∀ (x : M), LeftCancelMonoid.npow 0 x = 1

  Raising to the power (0 : ℕ) gives 1.

• npow_succ : ∀ (n : ℕ) (x : M), LeftCancelMonoid.npow (n + 1) x = x * LeftCancelMonoid.npow n x

  Raising to the power (n + 1 : ℕ) behaves as expected.

A monoid in which multiplication is left-cancellative.

class AddRightCancelMonoid (M : Type u) extends AddRightCancelSemigroup , Zero : Type u

• add : M → M → M
• add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)
• add_right_cancel : ∀ (a b c : M), a + b = c + b → a = c
• zero : M
• zero_add : ∀ (a : M), 0 + a = a

  Zero is a left neutral element for addition

• add_zero : ∀ (a : M), a + 0 = a

  Zero is a right neutral element for addition

• nsmul : ℕ → M → M

  Multiplication by a natural number.

• nsmul_zero : ∀ (x : M), AddRightCancelMonoid.nsmul 0 x = 0

  Multiplication by (0 : ℕ) gives 0.

• nsmul_succ : ∀ (n : ℕ) (x : M), AddRightCancelMonoid.nsmul (n + 1) x = x + AddRightCancelMonoid.nsmul n x

  Multiplication by (n + 1 : ℕ) behaves as expected.

An additive monoid in which addition is right-cancellative. Main examples are ℕ and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so AddRightCancelSemigroup is not enough.

class RightCancelMonoid (M : Type u) extends RightCancelSemigroup , One : Type u

• mul : M → M → M
• mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c)
• mul_right_cancel : ∀ (a b c : M), a * b = c * b → a = c
• one : M
• one_mul : ∀ (a : M), 1 * a = a

  One is a left neutral element for multiplication

• mul_one : ∀ (a : M), a * 1 = a

  One is a right neutral element for multiplication

• npow : ℕ → M → M

  Raising to the power of a natural number.

• npow_zero : ∀ (x : M), RightCancelMonoid.npow 0 x = 1

  Raising to the power (0 : ℕ) gives 1.

• npow_succ : ∀ (n : ℕ) (x : M), RightCancelMonoid.npow (n + 1) x = x * RightCancelMonoid.npow n x

  Raising to the power (n + 1 : ℕ) behaves as expected.

A monoid in which multiplication is right-cancellative.

class AddCancelMonoid (M : Type u) extends AddLeftCancelMonoid : Type u

• add : M → M → M
• add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)
• add_left_cancel : ∀ (a b c : M), a + b = a + c → b = c
• zero : M
• zero_add : ∀ (a : M), 0 + a = a
• add_zero : ∀ (a : M), a + 0 = a
• nsmul : ℕ → M → M
• nsmul_zero : ∀ (x : M), AddLeftCancelMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : M), AddLeftCancelMonoid.nsmul (n + 1) x = x + AddLeftCancelMonoid.nsmul n x
• add_right_cancel : ∀ (a b c : M), a + b = c + b → a = c

An additive monoid in which addition is cancellative on both sides. Main examples are ℕ and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so AddRightCancelMonoid is not enough.

class CancelMonoid (M : Type u) extends LeftCancelMonoid : Type u

• mul : M → M → M
• mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c)
• mul_left_cancel : ∀ (a b c : M), a * b = a * c → b = c
• one : M
• one_mul : ∀ (a : M), 1 * a = a
• mul_one : ∀ (a : M), a * 1 = a
• npow : ℕ → M → M
• npow_zero : ∀ (x : M), LeftCancelMonoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : M), LeftCancelMonoid.npow (n + 1) x = x * LeftCancelMonoid.npow n x
• mul_right_cancel : ∀ (a b c : M), a * b = c * b → a = c

A monoid in which multiplication is cancellative.

class AddCancelCommMonoid (M : Type u) extends AddLeftCancelMonoid : Type u

• add : M → M → M
• add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)
• add_left_cancel : ∀ (a b c : M), a + b = a + c → b = c
• zero : M
• zero_add : ∀ (a : M), 0 + a = a
• add_zero : ∀ (a : M), a + 0 = a
• nsmul : ℕ → M → M
• nsmul_zero : ∀ (x : M), AddLeftCancelMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : M), AddLeftCancelMonoid.nsmul (n + 1) x = x + AddLeftCancelMonoid.nsmul n x
• add_comm : ∀ (a b : M), a + b = b + a

  Addition is commutative in an additive commutative semigroup.

Commutative version of AddCancelMonoid.

class CancelCommMonoid (M : Type u) extends LeftCancelMonoid : Type u

• mul : M → M → M
• mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c)
• mul_left_cancel : ∀ (a b c : M), a * b = a * c → b = c
• one : M
• one_mul : ∀ (a : M), 1 * a = a
• mul_one : ∀ (a : M), a * 1 = a
• npow : ℕ → M → M
• npow_zero : ∀ (x : M), LeftCancelMonoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : M), LeftCancelMonoid.npow (n + 1) x = x * LeftCancelMonoid.npow n x
• mul_comm : ∀ (a b : M), a * b = b * a

  Multiplication is commutative in a commutative semigroup.

Commutative version of CancelMonoid.

theorem AddCancelCommMonoid.toAddCancelMonoid.proof_2 (M : Type u_1) [AddCancelCommMonoid M] (a : M) (b : M) (c : M) : a + b = c + b → a = c

theorem AddCancelCommMonoid.toAddCancelMonoid.proof_1 (M : Type u_1) [AddCancelCommMonoid M] : IsRightCancelAdd M

instance AddCancelCommMonoid.toAddCancelMonoid (M : Type u) [AddCancelCommMonoid M] : AddCancelMonoid M

Equations

• AddCancelCommMonoid.toAddCancelMonoid M = let src := (_ : IsRightCancelAdd M); AddCancelMonoid.mk (_ : ∀ (a b c : M), a + b = c + b → a = c)

instance CancelCommMonoid.toCancelMonoid (M : Type u) [CancelCommMonoid M] : CancelMonoid M

Equations

• CancelCommMonoid.toCancelMonoid M = let src := (_ : IsRightCancelMul M); CancelMonoid.mk (_ : ∀ (a b c : M), a * b = c * b → a = c)

theorem AddCancelMonoid.toIsCancelAdd.proof_1 (M : Type u_1) [AddCancelMonoid M] : IsCancelAdd M

instance AddCancelMonoid.toIsCancelAdd (M : Type u) [AddCancelMonoid M] : IsCancelAdd M

Any AddCancelMonoid G satisfies IsCancelAdd G.

Equations

• AddCancelMonoid.toIsCancelAdd = AddCancelMonoid.toIsCancelAdd.proof_1

instance CancelMonoid.toIsCancelMul (M : Type u) [CancelMonoid M] : IsCancelMul M

Any CancelMonoid G satisfies IsCancelMul G.

Equations

• CancelMonoid.toIsCancelMul = CancelMonoid.toIsCancelMul.proof_1

def zpowRec {M : Type u_2} [One M] [Mul M] [Inv M] : ℤ → M → M

The fundamental power operation in a group. zpowRec n a = a*a*...*a n times, for integer n. Use instead a ^ n, which has better definitional behavior.

Equations

• zpowRec x x = match x, x with | Int.ofNat n, a => npowRec n a | Int.negSucc n, a => (npowRec (Nat.succ n) a)⁻¹

def zsmulRec {M : Type u_2} [Zero M] [Add M] [Neg M] : ℤ → M → M

The fundamental scalar multiplication in an additive group. zpowRec n a = a+a+...+a n times, for integer n. Use instead n • a, which has better definitional behavior.

Equations

• zsmulRec x x = match x, x with | Int.ofNat n, a => nsmulRec n a | Int.negSucc n, a => -nsmulRec (Nat.succ n) a

class InvolutiveNeg (A : Type u_2) extends Neg : Type u_2

• neg : A → A
• neg_neg : ∀ (x : A), - -x = x

Auxiliary typeclass for types with an involutive Neg.

class InvolutiveInv (G : Type u_2) extends Inv : Type u_2

• inv : G → G
• inv_inv : ∀ (x : G), x⁻¹⁻¹ = x

Auxiliary typeclass for types with an involutive Inv.

@[simp]

theorem neg_neg {G : Type u_1} [InvolutiveNeg G] (a : G) : - -a = a

@[simp]

theorem inv_inv {G : Type u_1} [InvolutiveInv G] (a : G) : a⁻¹⁻¹ = a

Design note on DivInvMonoid/SubNegMonoid and DivisionMonoid/SubtractionMonoid

Those two pairs of made-up classes fulfill slightly different roles.

DivInvMonoid/SubNegMonoid provides the minimum amount of information to define the ℤ action (zpow or zsmul). Further, it provides a div field, matching the forgetful inheritance pattern. This is useful to shorten extension clauses of stronger structures (Group, GroupWithZero, DivisionRing, Field) and for a few structures with a rather weak pseudo-inverse (Matrix).

DivisionMonoid/SubtractionMonoid is targeted at structures with stronger pseudo-inverses. It is an ad hoc collection of axioms that are mainly respected by three things:

• Groups
• Groups with zero
• The pointwise monoids Set α, Finset α, Filter α

It acts as a middle ground for structures with an inversion operator that plays well with multiplication, except for the fact that it might not be a true inverse (a / a ≠ 1 in general). The axioms are pretty arbitrary (many other combinations are equivalent to it), but they are independent:

• Without DivisionMonoid.div_eq_mul_inv, you can define / arbitrarily.
• Without DivisionMonoid.inv_inv, you can consider WithTop Unit with a⁻¹ = ⊤ for all a.
• Without DivisionMonoid.mul_inv_rev, you can consider WithTop α with a⁻¹ = a for all a where α non commutative.
• Without DivisionMonoid.inv_eq_of_mul, you can consider any CommMonoid with a⁻¹ = a for all a.

As a consequence, a few natural structures do not fit in this framework. For example, ENNReal respects everything except for the fact that (0 * ∞)⁻¹ = 0⁻¹ = ∞ while ∞⁻¹ * 0⁻¹ = 0 * ∞ = 0.

def DivInvMonoid.div' {G : Type u} [Monoid G] [Inv G] (a : G) (b : G) : G

In a class equipped with instances of both Monoid and Inv, this definition records what the default definition for Div would be: a * b⁻¹. This is later provided as the default value for the Div instance in DivInvMonoid.

We keep it as a separate definition rather than inlining it in DivInvMonoid so that the Div field of individual DivInvMonoids constructed using that default value will not be unfolded at .instance transparency.

Equations

• DivInvMonoid.div' a b = a * b⁻¹

class DivInvMonoid (G : Type u) extends Monoid , Inv , Div : Type u

• mul : G → G → G
• mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
• one : G
• one_mul : ∀ (a : G), 1 * a = a
• mul_one : ∀ (a : G), a * 1 = a
• npow : ℕ → G → G
• npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = x * Monoid.npow n x
• inv : G → G
• div : G → G → G
• div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹

  a / b := a * b⁻¹

• zpow : ℤ → G → G

  The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1

  a ^ 0 = 1

• zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a

  a ^ (n + 1) = a * a ^ n

• zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹

  a ^ -(n + 1) = (a ^ (n + 1))⁻¹

A DivInvMonoid is a Monoid with operations / and ⁻¹ satisfying div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹.

This deduplicates the name div_eq_mul_inv. The default for div is such that a / b = a * b⁻¹ holds by definition.

Adding div as a field rather than defining a / b := a * b⁻¹ allows us to avoid certain classes of unification failures, for example: Let Foo X be a type with a ∀ X, Div (Foo X) instance but no ∀ X, Inv (Foo X), e.g. when Foo X is a EuclideanDomain. Suppose we also have an instance ∀ X [Cromulent X], GroupWithZero (Foo X). Then the (/) coming from GroupWithZero.div cannot be definitionally equal to the (/) coming from Foo.Div.

In the same way, adding a zpow field makes it possible to avoid definitional failures in diamonds. See the definition of Monoid and Note [forgetful inheritance] for more explanations on this.

def SubNegMonoid.sub' {G : Type u} [AddMonoid G] [Neg G] (a : G) (b : G) : G

In a class equipped with instances of both AddMonoid and Neg, this definition records what the default definition for Sub would be: a + -b. This is later provided as the default value for the Sub instance in SubNegMonoid.

We keep it as a separate definition rather than inlining it in SubNegMonoid so that the Sub field of individual SubNegMonoids constructed using that default value will not be unfolded at .instance transparency.

Equations

• SubNegMonoid.sub' a b = a + -b

class SubNegMonoid (G : Type u) extends AddMonoid , Neg , Sub : Type u

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

A SubNegMonoid is an AddMonoid with unary - and binary - operations satisfying sub_eq_add_neg : ∀ a b, a - b = a + -b.

The default for sub is such that a - b = a + -b holds by definition.

Adding sub as a field rather than defining a - b := a + -b allows us to avoid certain classes of unification failures, for example: Let foo X be a type with a ∀ X, Sub (Foo X) instance but no ∀ X, Neg (Foo X). Suppose we also have an instance ∀ X [Cromulent X], AddGroup (Foo X). Then the (-) coming from AddGroup.sub cannot be definitionally equal to the (-) coming from Foo.Sub.

In the same way, adding a zsmul field makes it possible to avoid definitional failures in diamonds. See the definition of AddMonoid and Note [forgetful inheritance] for more explanations on this.

instance DivInvMonoid.Pow {M : Type u_2} [DivInvMonoid M] : Pow M ℤ

Equations

• DivInvMonoid.Pow = { pow := fun x n => DivInvMonoid.zpow n x }

instance SubNegMonoid.SMulInt {M : Type u_2} [SubNegMonoid M] : SMul ℤ M

Equations

• SubNegMonoid.SMulInt = { smul := SubNegMonoid.zsmul }

@[simp]

theorem zsmul_eq_smul {G : Type u_1} [SubNegMonoid G] (n : ℤ) (x : G) : SubNegMonoid.zsmul n x = n • x

@[simp]

theorem zpow_eq_pow {G : Type u_1} [DivInvMonoid G] (n : ℤ) (x : G) : DivInvMonoid.zpow n x = x ^ n

@[simp]

theorem zero_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) : 0 • a = 0

@[simp]

theorem zpow_zero {G : Type u_1} [DivInvMonoid G] (a : G) : a ^ 0 = 1

theorem ofNat_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) (n : ℕ) : ↑n • a = n • a

abbrev ofNat_zsmul.match_1 (motive : ℕ → Prop) : (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive (Nat.succ n)) → motive x

Equations

• ofNat_zsmul.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n

theorem zpow_ofNat {G : Type u_1} [DivInvMonoid G] (a : G) (n : ℕ) : a ^ ↑n = a ^ n

@[simp]

theorem zpow_negSucc {G : Type u_1} [DivInvMonoid G] (a : G) (n : ℕ) : a ^ Int.negSucc n = (a ^ (n + 1))⁻¹

@[simp]

theorem negSucc_zsmul {G : Type u_2} [SubNegMonoid G] (a : G) (n : ℕ) : Int.negSucc n • a = -((n + 1) • a)

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

Subtracting an element is the same as adding by its negative. This is a duplicate of SubNegMonoid.sub_eq_mul_neg ensuring that the types unfold better.

theorem div_eq_mul_inv {G : Type u_1} [DivInvMonoid G] (a : G) (b : G) : a / b = a * b⁻¹

Dividing by an element is the same as multiplying by its inverse.

This is a duplicate of DivInvMonoid.div_eq_mul_inv ensuring that the types unfold better.

theorem division_def {G : Type u_1} [DivInvMonoid G] (a : G) (b : G) : a / b = a * b⁻¹

Alias of div_eq_mul_inv.

---

Dividing by an element is the same as multiplying by its inverse.

This is a duplicate of DivInvMonoid.div_eq_mul_inv ensuring that the types unfold better.

class NegZeroClass (G : Type u_2) extends Zero , Neg : Type u_2

• zero : G
• neg : G → G
• neg_zero : -0 = 0

Typeclass for expressing that -0 = 0.

class SubNegZeroMonoid (G : Type u_2) extends SubNegMonoid : Type u_2

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

A SubNegMonoid where -0 = 0.

class InvOneClass (G : Type u_2) extends One , Inv : Type u_2

• one : G
• inv : G → G
• inv_one : 1⁻¹ = 1

Typeclass for expressing that 1⁻¹ = 1.

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

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

A DivInvMonoid where 1⁻¹ = 1.

@[simp]

theorem neg_zero {G : Type u_1} [NegZeroClass G] : -0 = 0

@[simp]

theorem inv_one {G : Type u_1} [InvOneClass G] : 1⁻¹ = 1

class SubtractionMonoid (G : Type u) extends SubNegMonoid : Type u

• add : G → G → G
• add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
• zero : G
• zero_add : ∀ (a : G), 0 + a = a
• add_zero : ∀ (a : G), a + 0 = a
• nsmul : ℕ → G → G
• nsmul_zero : ∀ (x : G), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : G), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
• neg : G → G
• sub : G → G → G
• sub_eq_add_neg : ∀ (a b : G), a - b = a + -b
• zsmul : ℤ → G → G
• zsmul_zero' : ∀ (a : G), SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• neg_neg : ∀ (x : G), - -x = x
• neg_add_rev : ∀ (a b : G), -(a + b) = -b + -a
• neg_eq_of_add : ∀ (a b : G), a + b = 0 → -a = b

A SubtractionMonoid is a SubNegMonoid with involutive negation and such that -(a + b) = -b + -a and a + b = 0 → -a = b.

class DivisionMonoid (G : Type u) extends DivInvMonoid : Type u

• mul : G → G → G
• mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
• one : G
• one_mul : ∀ (a : G), 1 * a = a
• mul_one : ∀ (a : G), a * 1 = a
• npow : ℕ → G → G
• npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = x * Monoid.npow n x
• inv : G → G
• div : G → G → G
• div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹
• zpow : ℤ → G → G
• zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
• zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
• inv_inv : ∀ (x : G), x⁻¹⁻¹ = x
• mul_inv_rev : ∀ (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
• inv_eq_of_mul : ∀ (a b : G), a * b = 1 → a⁻¹ = b

A DivisionMonoid is a DivInvMonoid with involutive inversion and such that (a * b)⁻¹ = b⁻¹ * a⁻¹ and a * b = 1 → a⁻¹ = b.

This is the immediate common ancestor of Group and GroupWithZero.

@[simp]

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

@[simp]

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

theorem neg_eq_of_add_eq_zero_right {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} : a + b = 0 → -a = b

theorem inv_eq_of_mul_eq_one_right {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} : a * b = 1 → a⁻¹ = b

theorem neg_eq_of_add_eq_zero_left {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} (h : a + b = 0) : -b = a

theorem inv_eq_of_mul_eq_one_left {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} (h : a * b = 1) : b⁻¹ = a

theorem eq_neg_of_add_eq_zero_left {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} (h : a + b = 0) : a = -b

theorem eq_inv_of_mul_eq_one_left {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} (h : a * b = 1) : a = b⁻¹

class SubtractionCommMonoid (G : Type u) extends SubtractionMonoid : Type u

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

  Addition is commutative in an additive commutative semigroup.

Commutative SubtractionMonoid.

class DivisionCommMonoid (G : Type u) extends DivisionMonoid : Type u

• mul : G → G → G
• mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
• one : G
• one_mul : ∀ (a : G), 1 * a = a
• mul_one : ∀ (a : G), a * 1 = a
• npow : ℕ → G → G
• npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = x * Monoid.npow n x
• inv : G → G
• div : G → G → G
• div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹
• zpow : ℤ → G → G
• zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
• zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
• inv_inv : ∀ (x : G), x⁻¹⁻¹ = x
• mul_inv_rev : ∀ (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
• inv_eq_of_mul : ∀ (a b : G), a * b = 1 → a⁻¹ = b
• mul_comm : ∀ (a b : G), a * b = b * a

  Multiplication is commutative in a commutative semigroup.

Commutative DivisionMonoid.

This is the immediate common ancestor of CommGroup and CommGroupWithZero.

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

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

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 minumum proof obligations.

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

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

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 minumum proof obligations.

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem AddGroup.toSubtractionMonoid.proof_1 {G : Type u_1} [AddGroup G] (a : G) : - -a = a

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

Equations

• AddGroup.toSubtractionMonoid = SubtractionMonoid.mk (_ : ∀ (a : G), - -a = a) (_ : ∀ (a b : G), -(a + b) = -b + -a) (_ : ∀ (x x_1 : G), x + x_1 = 0 → -x = x_1)

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

Equations

• Group.toDivisionMonoid = DivisionMonoid.mk (_ : ∀ (a : G), a⁻¹⁻¹ = a) (_ : ∀ (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹) (_ : ∀ (x x_1 : G), x * x_1 = 1 → x⁻¹ = x_1)

theorem AddGroup.toAddCancelMonoid.proof_2 {G : Type u_1} [AddGroup G] (a : G) : 0 + a = a

theorem AddGroup.toAddCancelMonoid.proof_1 {G : Type u_1} [AddGroup G] (a : G) (b : G) (c : G) (h : a + b = a + c) : b = c

theorem AddGroup.toAddCancelMonoid.proof_4 {G : Type u_1} [AddGroup G] (x : G) : AddMonoid.nsmul 0 x = 0

theorem AddGroup.toAddCancelMonoid.proof_3 {G : Type u_1} [AddGroup G] (a : G) : a + 0 = a

theorem AddGroup.toAddCancelMonoid.proof_5 {G : Type u_1} [AddGroup G] (n : ℕ) (x : G) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

theorem AddGroup.toAddCancelMonoid.proof_6 {G : Type u_1} [AddGroup G] (a : G) (b : G) (c : G) (h : a + b = c + b) : a = c

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

Equations

• AddGroup.toAddCancelMonoid = let src := inst; AddCancelMonoid.mk (_ : ∀ (a b c : G), a + b = c + b → a = c)

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

Equations

• Group.toCancelMonoid = let src := inst; CancelMonoid.mk (_ : ∀ (a b c : G), a * b = c * b → a = c)

theorem AddGroup.toSubNegAddMonoid_injective {G : Type u_2} : Function.Injective (@AddGroup.toSubNegMonoid G)

theorem Group.toDivInvMonoid_injective {G : Type u_2} : Function.Injective (@Group.toDivInvMonoid G)

class AddCommGroup (G : Type u) extends AddGroup : Type u

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

  Addition is commutative in an additive commutative semigroup.

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

class CommGroup (G : Type u) extends Group : Type u

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

  Multiplication is commutative in a commutative semigroup.

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

theorem AddCommGroup.toAddGroup_injective {G : Type u} : Function.Injective (@AddCommGroup.toAddGroup G)

theorem CommGroup.toGroup_injective {G : Type u} : Function.Injective (@CommGroup.toGroup G)

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

Equations

• AddCommGroup.toAddCancelCommMonoid = let src := inst; let src_1 := AddGroup.toAddCancelMonoid; AddCancelCommMonoid.mk (_ : ∀ (a b : G), a + b = b + a)

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

Equations

• CommGroup.toCancelCommMonoid = let src := inst; let src_1 := Group.toCancelMonoid; CancelCommMonoid.mk (_ : ∀ (a b : G), a * b = b * a)

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

Equations

• AddCommGroup.toDivisionAddCommMonoid = let src := inst; let src_1 := AddGroup.toSubtractionMonoid; SubtractionCommMonoid.mk (_ : ∀ (a b : G), a + b = b + a)

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

Equations

• CommGroup.toDivisionCommMonoid = let src := inst; let src_1 := Group.toDivisionMonoid; DivisionCommMonoid.mk (_ : ∀ (a b : G), a * b = b * a)

We initialize all projections for @[simps] here, so that we don't have to do it in later files.

Note: the lemmas generated for the npow/zpow projections will not apply to x ^ y, since the argument order of these projections doesn't match the argument order of ^. The nsmul/zsmul lemmas will be correct.