Monoids

This file defines additive and multiplicative algebraic structures with a distinguished zero or one, up to and including monoids. Structures that do not require an identity are defined in Mathlib.Algebra.Group.Semigroup.

class AddZero (M : Type u_2) extends Zero M, Add M : Type u_2

Bundling an Add and Zero structure together without any axioms about their compatibility. See AddZeroClass for the additional assumption that 0 is an identity.

• zero : M
• add : M → M → M

class MulOne (M : Type u_2) extends One M, Mul M : Type u_2

Bundling a Mul and One structure together without any axioms about their compatibility. See MulOneClass for the additional assumption that 1 is an identity.

• one : M
• mul : M → M → M

theorem MulOne.ext_iff {M : Type u_2} {x y : MulOne M} : x = y ↔ One.one = One.one ∧ Mul.mul = Mul.mul

theorem MulOne.ext {M : Type u_2} {x y : MulOne M} (one : One.one = One.one) (mul : Mul.mul = Mul.mul) : x = y

theorem AddZero.ext_iff {M : Type u_2} {x y : AddZero M} : x = y ↔ Zero.zero = Zero.zero ∧ Add.add = Add.add

theorem AddZero.ext {M : Type u_2} {x y : AddZero M} (zero : Zero.zero = Zero.zero) (add : Add.add = Add.add) : x = y

class IsDedekindFiniteAddMonoid (M : Type u_2) [AddZero M] : Prop

An additive monoid is Dedekind-finite if every left inverse is also a right inverse. Also called von Neumann-finite or directly finite.

• add_eq_zero_symm {a b : M} : a + b = 0 → b + a = 0

class IsDedekindFiniteMonoid (M : Type u_2) [MulOne M] : Prop

A monoid is Dedekind-finite if every left inverse is also a right inverse. It is more common to talk about Dedekind-finite rings, but https://arxiv.org/abs/2102.01598 does define Dedekind-finite monoids in §2.2.

• mul_eq_one_symm {a b : M} : a * b = 1 → b * a = 1

theorem isDedekindFiniteAddMonoid_iff (M : Type u_2) [AddZero M] : IsDedekindFiniteAddMonoid M ↔ ∀ {a b : M}, a + b = 0 → b + a = 0

theorem isDedekindFiniteMonoid_iff (M : Type u_2) [MulOne M] : IsDedekindFiniteMonoid M ↔ ∀ {a b : M}, a * b = 1 → b * a = 1

theorem mul_eq_one_comm {M : Type u_2} [MulOne M] [IsDedekindFiniteMonoid M] {a b : M} : a * b = 1 ↔ b * a = 1

theorem add_eq_zero_comm {M : Type u_2} [AddZero M] [IsDedekindFiniteAddMonoid M] {a b : M} : a + b = 0 ↔ b + a = 0

@[instance 100]

instance instIsDedekindFiniteMonoidOfIsMulCommutative (M : Type u_2) [MulOne M] [IsMulCommutative M] : IsDedekindFiniteMonoid M

@[instance 100]

instance instIsDedekindFiniteAddMonoidOfIsAddCommutative (M : Type u_2) [AddZero M] [IsAddCommutative M] : IsDedekindFiniteAddMonoid M

class AddZeroClass (M : Type u_2) extends AddZero M : Type u_2

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

• 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

class MulOneClass (M : Type u_2) extends MulOne M : Type u_2

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

• 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

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

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

theorem AddZeroClass.ext_iff {M : Type u_2} {m₁ m₂ : AddZeroClass M} : m₁ = m₂ ↔ Add.add = Add.add

theorem MulOneClass.ext_iff {M : Type u_2} {m₁ m₂ : MulOneClass M} : m₁ = m₂ ↔ Mul.mul = Mul.mul

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

class IsUnital (A : Type u_2) [Mul A] : Prop

A multiplicative magma is unital if there exists a unit.

Note: Do not use this unless it is the only reasonable way to phrase or prove a statement. In general you should use NonUnitalRing, Ring, etc.

• isUnital : ∃ (u : A), ∀ (x : A), u * x = x ∧ x * u = x

theorem isUnital_iff (A : Type u_2) [Mul A] : IsUnital A ↔ ∃ (u : A), ∀ (x : A), u * x = x ∧ x * u = x

class IsNotUnital (A : Type u_2) [Mul A] : Prop

A multiplicative magma is not-unital if there does not exist a unit.

Note: Do not use this unless it is the only reasonable way to phrase or prove a statement. In general you should use NonUnitalRing, Ring, etc.

• isNotUnital (u : A) : ∃ (x : A), u * x ≠ x ∨ x * u ≠ x

theorem isNotUnital_iff (A : Type u_2) [Mul A] : IsNotUnital A ↔ ∀ (u : A), ∃ (x : A), u * x ≠ x ∨ x * u ≠ x

@[simp]

theorem not_isUnital_iff_isNotUnital {A : Type u_2} [Mul A] : ¬IsUnital A ↔ IsNotUnital A

@[simp]

theorem not_isNotUnital_iff_isUnital {A : Type u_2} [Mul A] : ¬IsNotUnital A ↔ IsUnital A

@[reducible, inline]

noncomputable abbrev IsUnital.toMulOneClass {A : Type u_2} [Mul A] [IsUnital A] : MulOneClass A

A unital magma is MulOneClass.

This constructor is primarily intended to be used within proofs since it creates bad definitional equalities.

Equations

• IsUnital.toMulOneClass = { one := ⋯.choose, toMul := inst✝¹, one_mul := ⋯, mul_one := ⋯ }

theorem MulOneClass.isUnital {A : Type u_2} [MulOneClass A] : IsUnital A

theorem npowRec_add {M : Type u_2} [One M] [Semigroup M] (m n : ℕ) (hn : n ≠ 0) (a : M) (ha : 1 * a = a) : npowRec (m + n) a = npowRec m a * npowRec n a

theorem nsmulRec_add {M : Type u_2} [Zero M] [AddSemigroup M] (m n : ℕ) (hn : n ≠ 0) (a : M) (ha : 0 + a = a) : nsmulRec (m + n) a = nsmulRec m a + nsmulRec n a

theorem npowRec_succ {M : Type u_2} [One M] [Semigroup M] (n : ℕ) (hn : n ≠ 0) (a : M) (ha : 1 * a = a) : npowRec (n + 1) a = a * npowRec n a

theorem nsmulRec_succ {M : Type u_2} [Zero M] [AddSemigroup M] (n : ℕ) (hn : n ≠ 0) (a : M) (ha : 0 + a = a) : nsmulRec (n + 1) a = a + nsmulRec n a

def LibraryNote.forgetful_inheritance : Batteries.Util.LibraryNote

Suppose that one can put two mathematical structures on a type, a rich one R and a poor one P, and that one can deduce the poor structure from the rich structure through a map F (called a forgetful functor) (think R = MetricSpace and P = TopologicalSpace). A possible implementation would be to have a type class rich containing a field R, a type class poor containing a field P, and an instance from rich to poor. However, this creates diamond problems, and a better approach is to let rich extend poor and have a field saying that F R = P.

To illustrate this, consider the pair MetricSpace / TopologicalSpace. Consider the topology on a product of two metric spaces. With the first approach, it could be obtained by going first from each metric space to its topology, and then taking the product topology. But it could also be obtained by considering the product metric space (with its sup distance) and then the topology coming from this distance. These would be the same topology, but not definitionally, which means that from the point of view of Lean's kernel, there would be two different TopologicalSpace instances on the product. This is not compatible with the way instances are designed and used: there should be at most one instance of a kind on each type. This approach has created an instance diamond that does not commute definitionally.

The second approach solves this issue. Now, a metric space contains both a distance, a topology, and a proof that the topology coincides with the one coming from the distance. When one defines the product of two metric spaces, one uses the sup distance and the product topology, and one has to give the proof that the sup distance induces the product topology. Following both sides of the instance diamond then gives rise (definitionally) to the product topology on the product space.

Another approach would be to have the rich type class take the poor type class as an instance parameter. It would solve the diamond problem, but it would lead to a blow up of the number of type classes one would need to declare to work with complicated classes, say a real inner product space, and would create exponential complexity when working with products of such complicated spaces, that are avoided by bundling things carefully as above.

Note that this description of this specific case of the product of metric spaces is oversimplified compared to mathlib, as there is an intermediate typeclass between MetricSpace and TopologicalSpace called UniformSpace. The above scheme is used at both levels, embedding a topology in the uniform space structure, and a uniform structure in the metric space structure.

Note also that, when P is a proposition, there is no such issue as any two proofs of P are definitionally equivalent in Lean.

To avoid boilerplate, there are some designs that can automatically fill the poor fields when creating a rich structure if one doesn't want to do something special about them. For instance, in the definition of metric spaces, default tactics fill the uniform space fields if they are not given explicitly. One can also have a helper function creating the rich structure from a structure with fewer fields, where the helper function fills the remaining fields. See for instance UniformSpace.ofCore or RealInnerProduct.ofCore.

For more details on this question, called the forgetful inheritance pattern, see Competing inheritance paths in dependent type theory: a case study in functional analysis.

Equations

• LibraryNote.forgetful_inheritance = default

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.

def npowBinRec {M : Type u_2} [One M] [Mul M] (k : ℕ) : M → M

Exponentiation by repeated squaring.

Equations

• npowBinRec k = npowBinRec.go k 1

def nsmulBinRec {M : Type u_2} [Zero M] [Add M] (k : ℕ) : M → M

Scalar multiplication by repeated self-addition, the additive version of exponentiation by repeated squaring.

Equations

• nsmulBinRec k = nsmulBinRec.go k 0

def nsmulBinRec.go {M : Type u_2} [Add M] (k : ℕ) : M → M → M

Auxiliary tail-recursive implementation for nsmulBinRec.

Equations

• nsmulBinRec.go k = Nat.binaryRec (motive := fun (x : ℕ) => M → M → M) (fun (y x : M) => y) (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) => fn (bif bn then y + x else y) (x + x)) k

def npowBinRec.go {M : Type u_2} [Mul M] (k : ℕ) : M → M → M

Auxiliary tail-recursive implementation for npowBinRec.

Equations

• npowBinRec.go k = Nat.binaryRec (motive := fun (x : ℕ) => M → M → M) (fun (y x : M) => y) (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) => fn (bif bn then y * x else y) (x * x)) k

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

A variant of npowRec which is a semigroup homomorphism from ℕ₊ to M.

Equations

• npowRec' 0 x✝ = 1
• npowRec' 1 x✝ = x✝
• npowRec' k.succ.succ x✝ = npowRec' (k + 1) x✝ * x✝

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

A variant of nsmulRec which is a semigroup homomorphism from ℕ₊ to M.

Equations

• nsmulRec' 0 x✝ = 0
• nsmulRec' 1 x✝ = x✝
• nsmulRec' k.succ.succ x✝ = nsmulRec' (k + 1) x✝ + x✝

theorem npowRec'_succ {M : Type u_2} [Mul M] [One M] {k : ℕ} : k ≠ 0 → ∀ (m : M), npowRec' (k + 1) m = npowRec' k m * m

theorem nsmulRec'_succ {M : Type u_2} [Add M] [Zero M] {k : ℕ} : k ≠ 0 → ∀ (m : M), nsmulRec' (k + 1) m = nsmulRec' k m + m

theorem npowRec'_two_mul {M : Type u_2} [Semigroup M] [One M] (k : ℕ) (m : M) : npowRec' (2 * k) m = npowRec' k (m * m)

theorem nsmulRec'_two_add {M : Type u_2} [AddSemigroup M] [Zero M] (k : ℕ) (m : M) : nsmulRec' (2 * k) m = nsmulRec' k (m + m)

theorem npowRec'_mul_comm {M : Type u_2} [Semigroup M] [One M] {k : ℕ} (k0 : k ≠ 0) (m : M) : m * npowRec' k m = npowRec' k m * m

theorem nsmulRec'_add_comm {M : Type u_2} [AddSemigroup M] [Zero M] {k : ℕ} (k0 : k ≠ 0) (m : M) : m + nsmulRec' k m = nsmulRec' k m + m

theorem npowRec_eq {M : Type u_2} [Semigroup M] [One M] (k : ℕ) (m : M) : npowRec (k + 1) m = 1 * npowRec' (k + 1) m

theorem nsmulRec_eq {M : Type u_2} [AddSemigroup M] [Zero M] (k : ℕ) (m : M) : nsmulRec (k + 1) m = 0 + nsmulRec' (k + 1) m

theorem npowBinRec.go_spec {M : Type u_2} [Semigroup M] [One M] (k : ℕ) (m n : M) : go (k + 1) m n = m * npowRec' (k + 1) n

theorem nsmulBinRec.go_spec {M : Type u_2} [AddSemigroup M] [Zero M] (k : ℕ) (m n : M) : go (k + 1) m n = m + nsmulRec' (k + 1) n

@[reducible, inline]

abbrev npowRecAuto {M : Type u_2} [Semigroup M] [One M] (k : ℕ) (m : M) : M

An abbreviation for npowRec with an additional typeclass assumption on associativity so that we can use @[csimp] to replace it with an implementation by repeated squaring in compiled code.

Equations

• npowRecAuto k m = npowRec k m

@[reducible, inline]

abbrev nsmulRecAuto {M : Type u_2} [AddSemigroup M] [Zero M] (k : ℕ) (m : M) : M

An abbreviation for nsmulRec with an additional typeclass assumptions on associativity so that we can use @[csimp] to replace it with an implementation by repeated doubling in compiled code as an automatic parameter.

Equations

• nsmulRecAuto k m = nsmulRec k m

@[reducible, inline]

abbrev npowBinRecAuto {M : Type u_2} [Semigroup M] [One M] (k : ℕ) (m : M) : M

An abbreviation for npowBinRec with an additional typeclass assumption on associativity so that we can use it in @[csimp] for more performant code generation.

Equations

• npowBinRecAuto k m = npowBinRec k m

@[reducible, inline]

abbrev nsmulBinRecAuto {M : Type u_2} [AddSemigroup M] [Zero M] (k : ℕ) (m : M) : M

An abbreviation for nsmulBinRec with an additional typeclass assumption on associativity so that we can use it in @[csimp] for more performant code generation as an automatic parameter.

Equations

• nsmulBinRecAuto k m = nsmulBinRec k m

@[csimp]

theorem npowRec_eq_npowBinRec : @npowRecAuto = @npowBinRecAuto

@[csimp]

theorem nsmulRec_eq_nsmulBinRec : @nsmulRecAuto = @nsmulBinRecAuto

theorem npowBinRec_zero {M : Type u_2} [Mul M] [One M] (m : M) : npowBinRec 0 m = 1

theorem nsmulBinRec_zero {M : Type u_2} [Add M] [Zero M] (m : M) : nsmulBinRec 0 m = 0

theorem npowBinRec_succ {M : Type u_2} [Semigroup M] [One M] (n : ℕ) (m : M) : npowBinRec (n + 1) m = npowBinRec n m * m

theorem nsmulBinRec_succ {M : Type u_2} [AddSemigroup M] [Zero M] (n : ℕ) (m : M) : nsmulBinRec (n + 1) m = nsmulBinRec n m + m

class NSMul (M : Type u_2) : Type u_2

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

• nsmul : ℕ → M → M

  Multiplication by a natural number. Set this to nsmulRec unless Module diamonds are possible.

class NPow (M : Type u_2) : Type u_2

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

• npow : ℕ → M → M

  Raising to the power of a natural number.

@[instance_reducible, defaultInstance 10000]

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

Equations

• NPow.toPow = { pow := fun (x : M) (n : ℕ) => NPow.npow n x }

@[instance_reducible]

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

Equations

• NSMul.toSMul = { smul := fun (n : ℕ) (x : M) => NSMul.nsmul n x }

@[instance_reducible]

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

Equations

• NPow.ofPow = { npow := fun (n : ℕ) (x : M) => Pow.pow x n }

@[instance_reducible]

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

Equations

• NSMul.ofSMul = { nsmul := fun (n : ℕ) (x : M) => SMul.smul n x }

class AddMonoid (M : Type u_2) extends AddSemigroup M, AddZeroClass M, NSMul M : Type u_2

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

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

  Multiplication by (0 : ℕ) gives 0.

• nsmul_succ (n : ℕ) (x : M) : (n + 1) • x = n • x + x

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

class Monoid (M : Type u_2) extends Semigroup M, MulOneClass M, NPow M : Type u_2

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

• 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) : x ^ 0 = 1

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

• npow_succ (n : ℕ) (x : M) : x ^ (n + 1) = x ^ n * x

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

theorem one_nsmul {M : Type u_2} [AddMonoid M] (a : M) : 1 • a = a

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

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

theorem mul_pow_mul {M : Type u_2} [Monoid M] (a b : M) (n : ℕ) : (a * b) ^ n * a = a * (b * a) ^ n

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

theorem pow_mul_comm' {M : Type u_2} [Monoid M] (a : M) (n : ℕ) : a ^ n * a = a * a ^ n

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

theorem pow_two {M : Type u_2} [Monoid M] (a : M) : a ^ 2 = a * a

Note that most of the lemmas about powers of two refer to it as sq.

theorem two_nsmul {M : Type u_2} [AddMonoid M] (a : M) : 2 • a = a + a

theorem sq {M : Type u_2} [Monoid M] (a : M) : a ^ 2 = a * a

Alias of pow_two.

---

Note that most of the lemmas about powers of two refer to it as sq.

theorem pow_three' {M : Type u_2} [Monoid M] (a : M) : a ^ 3 = a * a * a

theorem three'_nsmul {M : Type u_2} [AddMonoid M] (a : M) : 3 • a = a + a + a

theorem pow_three {M : Type u_2} [Monoid M] (a : M) : a ^ 3 = a * (a * a)

theorem three_nsmul {M : Type u_2} [AddMonoid M] (a : M) : 3 • a = a + (a + a)

@[simp]

theorem one_pow {M : Type u_2} [Monoid M] (n : ℕ) : 1 ^ n = 1

@[simp]

theorem nsmul_zero {M : Type u_2} [AddMonoid M] (n : ℕ) : n • 0 = 0

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

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

theorem pow_mul_comm {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) : a ^ m * a ^ n = a ^ n * a ^ m

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

theorem pow_mul {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) : a ^ (m * n) = (a ^ m) ^ n

theorem mul_nsmul {M : Type u_2} [AddMonoid M] (a : M) (m n : ℕ) : (m * n) • a = n • m • a

theorem pow_mul' {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) : a ^ (m * n) = (a ^ n) ^ m

theorem mul_nsmul' {M : Type u_2} [AddMonoid M] (a : M) (m n : ℕ) : (m * n) • a = m • n • a

theorem pow_right_comm {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) : (a ^ m) ^ n = (a ^ n) ^ m

theorem nsmul_left_comm {M : Type u_2} [AddMonoid M] (a : M) (m n : ℕ) : n • m • a = m • n • a

theorem IsLeftRegular.mul_eq_one_symm {M : Type u_2} [Monoid M] {a b : M} (reg : IsLeftRegular a) (eq : a * b = 1) : b * a = 1

theorem IsAddLeftRegular.add_eq_zero_symm {M : Type u_2} [AddMonoid M] {a b : M} (reg : IsAddLeftRegular a) (eq : a + b = 0) : b + a = 0

theorem IsRightRegular.mul_eq_one_symm {M : Type u_2} [Monoid M] {a b : M} (reg : IsRightRegular a) (eq : b * a = 1) : a * b = 1

theorem IsAddRightRegular.add_eq_zero_symm {M : Type u_2} [AddMonoid M] {a b : M} (reg : IsAddRightRegular a) (eq : b + a = 0) : a + b = 0

instance instIsDedekindFiniteMonoidOfIsLeftCancelMul (M : Type u_2) [Monoid M] [IsLeftCancelMul M] : IsDedekindFiniteMonoid M

instance instIsDedekindFiniteAddMonoidOfIsLeftCancelAdd (M : Type u_2) [AddMonoid M] [IsLeftCancelAdd M] : IsDedekindFiniteAddMonoid M

instance instIsDedekindFiniteMonoidOfIsRightCancelMul (M : Type u_2) [Monoid M] [IsRightCancelMul M] : IsDedekindFiniteMonoid M

instance instIsDedekindFiniteAddMonoidOfIsRightCancelAdd (M : Type u_2) [AddMonoid M] [IsRightCancelAdd M] : IsDedekindFiniteAddMonoid M

theorem IsDedekindFiniteMonoid.of_exists_self_mul_eq_one (M : Type u_2) [Monoid M] (ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), y * z = 1) : IsDedekindFiniteMonoid M

A monoid is Dedekind-finite if every element with a left inverse also has a right inverse.

theorem IsDedekindFiniteAddMonoid.of_exists_self_add_eq_zero (M : Type u_2) [AddMonoid M] (ex : ∀ (x y : M), x + y = 0 → ∃ (z : M), y + z = 0) : IsDedekindFiniteAddMonoid M

theorem IsDedekindFiniteMonoid.of_exists_mul_self_eq_one (M : Type u_2) [Monoid M] (ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), z * x = 1) : IsDedekindFiniteMonoid M

A monoid is Dedekind-finite if every element with a right inverse also has a left inverse.

theorem IsDedekindFiniteAddMonoid.of_exists_add_self_eq_zero (M : Type u_2) [AddMonoid M] (ex : ∀ (x y : M), x + y = 0 → ∃ (z : M), z + x = 0) : IsDedekindFiniteAddMonoid M

@[reducible, inline]

noncomputable abbrev IsUnital.toMonoid {A : Type u_2} [Semigroup A] [IsUnital A] : Monoid A

A unital semigroup is a monoid.

This constructor is primarily intended to be used within proofs since it creates bad definitional equalities.

Equations

• IsUnital.toMonoid = { toSemigroup := inst✝¹, toOne := IsUnital.toMulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

class IsAddTorsionFree (M : Type u_2) [AddMonoid M] : Prop

An additive monoid is torsion-free if scalar multiplication by every non-zero element n : ℕ is injective.

• nsmul_right_injective ⦃n : ℕ⦄ (hn : n ≠ 0) : Function.Injective fun (a : M) => n • a

theorem isAddTorsionFree_iff (M : Type u_2) [AddMonoid M] : IsAddTorsionFree M ↔ ∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun (a : M) => n • a

class IsMulTorsionFree (M : Type u_2) [Monoid M] : Prop

A monoid is torsion-free if power by every non-zero element n : ℕ is injective.

• pow_left_injective ⦃n : ℕ⦄ (hn : n ≠ 0) : Function.Injective fun (a : M) => a ^ n

theorem isMulTorsionFree_iff (M : Type u_2) [Monoid M] : IsMulTorsionFree M ↔ ∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun (a : M) => a ^ n

class AddCommMonoid (M : Type u_2) extends AddMonoid M, AddCommSemigroup M : Type u_2

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

• 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) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : M) : (n + 1) • x = n • x + x
• add_comm (a b : M) : a + b = b + a

class CommMonoid (M : Type u_2) extends Monoid M, CommSemigroup M : Type u_2

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

• 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) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : M) : x ^ (n + 1) = x ^ n * x
• mul_comm (a b : M) : a * b = b * a

instance instIsDedekindFiniteMonoid (M : Type u_2) [CommMonoid M] : IsDedekindFiniteMonoid M

Shortcut instance for IsCommutativeHMul M → IsDedekindFiniteMonoid M.

This is assigned default rather than low priority because it gives the most common examples of Dedekind-finite monoids and is used the most often. Benchmark results indicate default priority performs better than low or high priority.

instance instIsDedekindFiniteAddMonoid (M : Type u_2) [AddCommMonoid M] : IsDedekindFiniteAddMonoid M

class AddLeftCancelMonoid (M : Type u_2) extends AddMonoid M, AddLeftCancelSemigroup M : Type u_2

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.

• 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) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : M) : (n + 1) • x = n • x + x
• add_left_cancel (a : M) : IsAddLeftRegular a

class LeftCancelMonoid (M : Type u_2) extends Monoid M, LeftCancelSemigroup M : Type u_2

A monoid in which multiplication is left-cancellative.

• 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) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : M) : x ^ (n + 1) = x ^ n * x
• mul_left_cancel (a : M) : IsLeftRegular a

class AddRightCancelMonoid (M : Type u_2) extends AddMonoid M, AddRightCancelSemigroup M : Type u_2

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.

• 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) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : M) : (n + 1) • x = n • x + x
• add_right_cancel (a : M) : IsAddRightRegular a

class RightCancelMonoid (M : Type u_2) extends Monoid M, RightCancelSemigroup M : Type u_2

A monoid in which multiplication is right-cancellative.

• 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) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : M) : x ^ (n + 1) = x ^ n * x
• mul_right_cancel (a : M) : IsRightRegular a

class AddCancelMonoid (M : Type u_2) extends AddLeftCancelMonoid M, AddRightCancelMonoid M : Type u_2

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.

• 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) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : M) : (n + 1) • x = n • x + x
• add_left_cancel (a : M) : IsAddLeftRegular a
• add_right_cancel (a : M) : IsAddRightRegular a

class CancelMonoid (M : Type u_2) extends LeftCancelMonoid M, RightCancelMonoid M : Type u_2

A monoid in which multiplication is cancellative.

• 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) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : M) : x ^ (n + 1) = x ^ n * x
• mul_left_cancel (a : M) : IsLeftRegular a
• mul_right_cancel (a : M) : IsRightRegular a

class AddCancelCommMonoid (M : Type u_2) extends AddCommMonoid M, AddLeftCancelMonoid M : Type u_2

Commutative version of AddCancelMonoid.

• 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) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : M) : (n + 1) • x = n • x + x
• add_comm (a b : M) : a + b = b + a
• add_left_cancel (a : M) : IsAddLeftRegular a

class CancelCommMonoid (M : Type u_2) extends CommMonoid M, LeftCancelMonoid M : Type u_2

Commutative version of CancelMonoid.

• 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) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : M) : x ^ (n + 1) = x ^ n * x
• mul_comm (a b : M) : a * b = b * a
• mul_left_cancel (a : M) : IsLeftRegular a

@[instance_reducible, instance 100]

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

Equations

• CancelCommMonoid.toCancelMonoid M = { toLeftCancelMonoid := inst✝.toLeftCancelMonoid, toIsRightCancelMul := ⋯ }

@[instance_reducible, instance 100]

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

Equations

• AddCancelCommMonoid.toAddCancelMonoid M = { toAddLeftCancelMonoid := inst✝.toAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }

@[instance 100]

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

Any CancelMonoid G satisfies IsCancelMul G.

@[instance 100]

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

Any AddCancelMonoid G satisfies IsCancelAdd G.

We initialize the projections for the monoid 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.