Division monoids

This file defines additive and multiplicative structures with division, inversion, subtraction, or negation, up to DivisionCommMonoid and SubtractionCommMonoid. Group structures are defined in Mathlib.Algebra.Group.Defs.

def zpowRec {G : Type u_1} [One G] [Mul G] [Inv G] (npow : ℕ → G → G := npowRec) : ℤ → G → G

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.

def zsmulRec {G : Type u_1} [Zero G] [Add G] [Neg G] (nsmul : ℕ → G → G := nsmulRec) : ℤ → G → G

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.

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

Auxiliary typeclass for types with an involutive Neg.

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

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

Auxiliary typeclass for types with an involutive Inv.

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

@[simp]

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

@[simp]

theorem neg_neg {G : Type u_1} [InvolutiveNeg 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 α noncommutative.
• 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_2} [Monoid G] [Inv G] (a 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.

def SubNegMonoid.sub' {G : Type u_2} [AddMonoid G] [Neg G] (a 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.

class ZSMul (G : Type u_2) : Type u_2

ZSMul is an implementation detail of SubNegMonoid. It is needed because it is impossible to extend SMUl ℕ M and SMul ℤ M at the same time.

• zsmul : ℤ → G → G

  Multiplication by an integer. Set this to zsmulRec unless Module diamonds are possible.

class ZPow (G : Type u_2) : Type u_2

ZPow is an implementation detail of DivInvMonoid. It is needed because it is impossible to extend Pow M ℕ and Pow M ℤ at the same time.

• zpow : ℤ → G → G

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

@[instance_reducible]

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

@[instance_reducible]

instance ZSMul.toSMul {M : Type u_2} [ZSMul M] : SMul ℤ M

@[instance_reducible]

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

@[instance_reducible]

instance ZSMul.ofSMul {M : Type u_2} [SMul ℤ M] : ZSMul M

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

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.

• 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⁻¹

  a / b := a * b⁻¹

• zpow_zero' (a : G) : a ^ 0 = 1

  a ^ 0 = 1

• zpow_succ' (n : ℕ) (a : G) : a ^ ↑n.succ = a ^ ↑n * a

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

• zpow_neg' (n : ℕ) (a : G) : a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹

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

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

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.

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

class IsAddCyclic (G : Type u_2) [SMul ℤ G] : Prop

A group is called cyclic if it is generated by a single element.

Wikidata Q245462

• exists_zsmul_surjective : ∃ (g : G), Function.Surjective fun (x : ℤ) => x • g

class IsCyclic (G : Type u_2) [Pow G ℤ] : Prop

A group is called cyclic if it is generated by a single element.

Wikidata Q245462

• exists_zpow_surjective : ∃ (g : G), Function.Surjective fun (x : ℤ) => g ^ x

theorem exists_zpow_surjective (G : Type u_2) [Pow G ℤ] [IsCyclic G] : ∃ (g : G), Function.Surjective fun (x : ℤ) => g ^ x

theorem exists_zsmul_surjective (G : Type u_2) [SMul ℤ G] [IsAddCyclic G] : ∃ (g : G), Function.Surjective fun (x : ℤ) => x • g

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[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_1} [SubNegMonoid G] (a : G) (n : ℕ) : Int.negSucc n • a = -((n + 1) • a)

theorem div_eq_mul_inv {G : Type u_1} [DivInvMonoid G] (a 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 sub_eq_add_neg {G : Type u_1} [SubNegMonoid G] (a 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_add_neg ensuring that the types unfold better.

theorem division_def {G : Type u_1} [DivInvMonoid G] (a 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.

theorem inv_eq_one_div {G : Type u_1} [DivInvMonoid G] (x : G) : x⁻¹ = 1 / x

theorem neg_eq_zero_sub {G : Type u_1} [SubNegMonoid G] (x : G) : -x = 0 - x

theorem mul_div_assoc {G : Type u_1} [DivInvMonoid G] (a b c : G) : a * b / c = a * (b / c)

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

@[simp]

theorem one_div {G : Type u_1} [DivInvMonoid G] (a : G) : 1 / a = a⁻¹

@[simp]

theorem zero_sub {G : Type u_1} [SubNegMonoid G] (a : G) : 0 - a = -a

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

@[simp]

theorem one_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) : 1 • a = a

theorem zpow_two {G : Type u_1} [DivInvMonoid G] (a : G) : a ^ 2 = a * a

theorem two_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) : 2 • a = a + a

theorem zpow_neg_one {G : Type u_1} [DivInvMonoid G] (x : G) : x ^ (-1) = x⁻¹

theorem neg_one_zsmul {G : Type u_1} [SubNegMonoid G] (x : G) : -1 • x = -x

theorem zpow_neg_coe_of_pos {G : Type u_1} [DivInvMonoid G] (a : G) {n : ℕ} : 0 < n → a ^ (-↑n) = (a ^ n)⁻¹

theorem zsmul_neg_coe_of_pos {G : Type u_1} [SubNegMonoid G] (a : G) {n : ℕ} : 0 < n → -↑n • a = -(n • a)

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

Typeclass for expressing that -0 = 0.

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

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

A SubNegMonoid where -0 = 0.

• 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_zero : -0 = 0

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

Typeclass for expressing that 1⁻¹ = 1.

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

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

A DivInvMonoid where 1⁻¹ = 1.

• 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_one : 1⁻¹ = 1

@[simp]

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

@[simp]

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

class SubtractionMonoid (G : Type u_2) extends SubNegMonoid G, InvolutiveNeg G : Type u_2

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

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

  Despite the asymmetry of neg_eq_of_add, the symmetric version is true thanks to the involutivity of negation.

class DivisionMonoid (G : Type u_2) extends DivInvMonoid G, InvolutiveInv G : Type u_2

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.

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

  Despite the asymmetry of inv_eq_of_mul, the symmetric version is true thanks to the involutivity of inversion.

@[simp]

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

@[simp]

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

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

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

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

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

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

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

class SubtractionCommMonoid (G : Type u_2) extends SubtractionMonoid G, AddCommMonoid G : Type u_2

Commutative SubtractionMonoid.

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

class DivisionCommMonoid (G : Type u_2) extends DivisionMonoid G, CommMonoid G : Type u_2

Commutative DivisionMonoid.

This is the immediate common ancestor of CommGroup and CommGroupWithZero.

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

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.