# 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 `Mathlib/Algebra/Group/Basic.lean`.

We 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`.

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

A mixin for left cancellative multiplication.

- mul_left_cancel (a : G) : IsLeftRegular a

  Multiplication is left cancellative (i.e. left regular).

Instances

source
theorem isLeftCancelMul_iff (G : Type u) [Mul G] :
IsLeftCancelMul G ↔ ∀ (a : G), IsLeftRegular a
source
class IsRightCancelMul (G : Type u) [Mul G] :
Prop

A mixin for right cancellative multiplication.

- mul_right_cancel (a : G) : IsRightRegular a

  Multiplication is right cancellative (i.e. right regular).

Instances

source
theorem isRightCancelMul_iff (G : Type u) [Mul G] :
IsRightCancelMul G ↔ ∀ (a : G), IsRightRegular a
source
class IsCancelMul (G : Type u) [Mul G] extends IsLeftCancelMul G, IsRightCancelMul G :
Prop

A mixin for cancellative multiplication.

- mul_left_cancel (a : G) : IsLeftRegular a
- mul_right_cancel (a : G) : IsRightRegular a

Instances

source
theorem isCancelMul_iff (G : Type u) [Mul G] :
IsCancelMul G ↔ IsLeftCancelMul G ∧ IsRightCancelMul G
source
class IsLeftCancelAdd (G : Type u) [Add G] :
Prop

A mixin for left cancellative addition.

- add_left_cancel (a : G) : IsAddLeftRegular a

  Addition is left cancellative (i.e. left regular).

Instances

source
theorem isLeftCancelAdd_iff (G : Type u) [Add G] :
IsLeftCancelAdd G ↔ ∀ (a : G), IsAddLeftRegular a
source
class IsRightCancelAdd (G : Type u) [Add G] :
Prop

A mixin for right cancellative addition.

- add_right_cancel (a : G) : IsAddRightRegular a

  Addition is right cancellative (i.e. right regular).

Instances

source
theorem isRightCancelAdd_iff (G : Type u) [Add G] :
IsRightCancelAdd G ↔ ∀ (a : G), IsAddRightRegular a
source
class IsCancelAdd (G : Type u) [Add G] extends IsLeftCancelAdd G, IsRightCancelAdd G :
Prop

A mixin for cancellative addition.

- add_left_cancel (a : G) : IsAddLeftRegular a
- add_right_cancel (a : G) : IsAddRightRegular a

Instances

source
theorem isCancelAdd_iff (G : Type u) [Add G] :
IsCancelAdd G ↔ IsLeftCancelAdd G ∧ IsRightCancelAdd G
source
theorem isCancelMul_iff_forall_isRegular {R : Type u_2} [Mul R] :
IsCancelMul R ↔ ∀ (r : R), IsRegular r
source
theorem isCancelAdd_iff_forall_isAddRegular {R : Type u_2} [Add R] :
IsCancelAdd R ↔ ∀ (r : R), IsAddRegular r
source
theorem IsLeftRegular.all {R : Type u_2} [Mul R] [IsLeftCancelMul R] (g : R) :
IsLeftRegular g

If all multiplications cancel on the left then every element is left-regular.

source
theorem IsAddLeftRegular.all {R : Type u_2} [Add R] [IsLeftCancelAdd R] (g : R) :
IsAddLeftRegular g

If all additions cancel on the left then every element is add-left-regular.

source
theorem IsRightRegular.all {R : Type u_2} [Mul R] [IsRightCancelMul R] (g : R) :
IsRightRegular g

If all multiplications cancel on the right then every element is right-regular.

source
theorem IsAddRightRegular.all {R : Type u_2} [Add R] [IsRightCancelAdd R] (g : R) :
IsAddRightRegular g

If all additions cancel on the right then every element is add-right-regular.

source
theorem IsRegular.all {R : Type u_2} [Mul R] [IsCancelMul R] (g : R) :
IsRegular g

If all multiplications cancel then every element is regular.

source
theorem IsAddRegular.all {R : Type u_2} [Add R] [IsCancelAdd R] (g : R) :
IsAddRegular g

If all additions cancel then every element is add-regular.

source
theorem mul_left_cancel {G : Type u_1} [Mul G] [IsLeftCancelMul G] {a b c : G} :
a * b = a * c → b = c
source
theorem add_left_cancel {G : Type u_1} [Add G] [IsLeftCancelAdd G] {a b c : G} :
a + b = a + c → b = c
source
theorem mul_left_cancel_iff {G : Type u_1} [Mul G] [IsLeftCancelMul G] {a b c : G} :
a * b = a * c ↔ b = c
source
theorem add_left_cancel_iff {G : Type u_1} [Add G] [IsLeftCancelAdd G] {a b c : G} :
a + b = a + c ↔ b = c
source
theorem mul_right_injective {G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) :
Function.Injective fun (x : G) => a * x
source
theorem add_right_injective {G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) :
Function.Injective fun (x : G) => a + x
source
@[simp]
theorem mul_right_inj {G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) {b c : G} :
a * b = a * c ↔ b = c
source
@[simp]
theorem add_right_inj {G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) {b c : G} :
a + b = a + c ↔ b = c
source
theorem mul_ne_mul_right {G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) {b c : G} :
a * b ≠ a * c ↔ b ≠ c
source
theorem add_ne_add_right {G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) {b c : G} :
a + b ≠ a + c ↔ b ≠ c
source
theorem mul_right_cancel {G : Type u_1} [Mul G] [IsRightCancelMul G] {a b c : G} :
a * b = c * b → a = c
source
theorem add_right_cancel {G : Type u_1} [Add G] [IsRightCancelAdd G] {a b c : G} :
a + b = c + b → a = c
source
theorem mul_right_cancel_iff {G : Type u_1} [Mul G] [IsRightCancelMul G] {a b c : G} :
b * a = c * a ↔ b = c
source
theorem add_right_cancel_iff {G : Type u_1} [Add G] [IsRightCancelAdd G] {a b c : G} :
b + a = c + a ↔ b = c
source
theorem mul_left_injective {G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) :
Function.Injective fun (x : G) => x * a
source
theorem add_left_injective {G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) :
Function.Injective fun (x : G) => x + a
source
@[simp]
theorem mul_left_inj {G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) {b c : G} :
b * a = c * a ↔ b = c
source
@[simp]
theorem add_left_inj {G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) {b c : G} :
b + a = c + a ↔ b = c
source
theorem mul_ne_mul_left {G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) {b c : G} :
b * a ≠ c * a ↔ b ≠ c
source
theorem add_ne_add_left {G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) {b c : G} :
b + a ≠ c + a ↔ b ≠ c
source
class Semigroup (G : Type u) extends Mul G :
Type u

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

- mul : G → G → G
- mul_assoc (a b c : G) : a * b * c = a * (b * c)

  Multiplication is associative

Instances

source
theorem Semigroup.ext {G : Type u} {x y : Semigroup G} (mul : Mul.mul = Mul.mul) :
x = y
source
theorem Semigroup.ext_iff {G : Type u} {x y : Semigroup G} :
x = y ↔ Mul.mul = Mul.mul
source
class AddSemigroup (G : Type u) extends Add G :
Type u

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

- add : G → G → G
- add_assoc (a b c : G) : a + b + c = a + (b + c)

  Addition is associative

Instances

source
theorem AddSemigroup.ext_iff {G : Type u} {x y : AddSemigroup G} :
x = y ↔ Add.add = Add.add
source
theorem AddSemigroup.ext {G : Type u} {x y : AddSemigroup G} (add : Add.add = Add.add) :
x = y
source
theorem mul_assoc {G : Type u_1} [Semigroup G] (a b c : G) :
a * b * c = a * (b * c)
source
theorem add_assoc {G : Type u_1} [AddSemigroup G] (a b c : G) :
a + b + c = a + (b + c)
source
class AddCommMagma (G : Type u) extends Add G :
Type u

A commutative additive magma is a type with an addition which commutes.

- add : G → G → G
- add_comm (a b : G) : a + b = b + a

  Addition is commutative in an commutative additive magma.

Instances

source
theorem AddCommMagma.ext_iff {G : Type u} {x y : AddCommMagma G} :
x = y ↔ Add.add = Add.add
source
theorem AddCommMagma.ext {G : Type u} {x y : AddCommMagma G} (add : Add.add = Add.add) :
x = y
source
class CommMagma (G : Type u) extends Mul G :
Type u

A commutative multiplicative magma is a type with a multiplication which commutes.

- mul : G → G → G
- mul_comm (a b : G) : a * b = b * a

  Multiplication is commutative in a commutative multiplicative magma.

Instances

source
theorem CommMagma.ext_iff {G : Type u} {x y : CommMagma G} :
x = y ↔ Mul.mul = Mul.mul
source
theorem CommMagma.ext {G : Type u} {x y : CommMagma G} (mul : Mul.mul = Mul.mul) :
x = y
source
class CommSemigroup (G : Type u) extends Semigroup G, CommMagma G :
Type u

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

- 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

Instances

source
theorem CommSemigroup.ext {G : Type u} {x y : CommSemigroup G} (mul : Mul.mul = Mul.mul) :
x = y
source
theorem CommSemigroup.ext_iff {G : Type u} {x y : CommSemigroup G} :
x = y ↔ Mul.mul = Mul.mul
source
class AddCommSemigroup (G : Type u) extends AddSemigroup G, AddCommMagma G :
Type u

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

- 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

Instances

source
theorem AddCommSemigroup.ext {G : Type u} {x y : AddCommSemigroup G} (add : Add.add = Add.add) :
x = y
source
theorem AddCommSemigroup.ext_iff {G : Type u} {x y : AddCommSemigroup G} :
x = y ↔ Add.add = Add.add
source
theorem mul_comm {G : Type u_1} [CommMagma G] (a b : G) :
a * b = b * a
source
theorem add_comm {G : Type u_1} [AddCommMagma G] (a b : G) :
a + b = b + a
source
@[simp]
theorem isLeftRegular_iff_isRegular {G : Type u_1} [CommMagma G] {a : G} :
IsLeftRegular a ↔ IsRegular a
source
@[simp]
theorem isRightRegular_iff_isRegular {G : Type u_1} [CommMagma G] {a : G} :
IsRightRegular a ↔ IsRegular a
source
theorem CommMagma.IsRightCancelMul.toIsLeftCancelMul (G : Type u) [CommMagma G] [IsRightCancelMul G] :
IsLeftCancelMul G

Any `CommMagma G` that satisfies `IsRightCancelMul G` also satisfies `IsLeftCancelMul G`.

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

Any `AddCommMagma G` that satisfies `IsRightCancelAdd G` also satisfies `IsLeftCancelAdd G`.

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

Any `CommMagma G` that satisfies `IsLeftCancelMul G` also satisfies `IsRightCancelMul G`.

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

Any `AddCommMagma G` that satisfies `IsLeftCancelAdd G` also satisfies `IsRightCancelAdd G`.

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

Any `CommMagma G` that satisfies `IsLeftCancelMul G` also satisfies `IsCancelMul G`.

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

Any `AddCommMagma G` that satisfies `IsLeftCancelAdd G` also satisfies `IsCancelAdd G`.

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

Any `CommMagma G` that satisfies `IsRightCancelMul G` also satisfies `IsCancelMul G`.

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

Any `AddCommMagma G` that satisfies `IsRightCancelAdd G` also satisfies `IsCancelAdd G`.

source
class LeftCancelSemigroup (G : Type u) extends Semigroup G, IsLeftCancelMul G :
Type u

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

- mul : G → G → G
- mul_assoc (a b c : G) : a * b * c = a * (b * c)
- mul_left_cancel (a : G) : IsLeftRegular a

Instances

source
theorem LeftCancelSemigroup.ext_iff {G : Type u} {x y : LeftCancelSemigroup G} :
x = y ↔ Mul.mul = Mul.mul
source
theorem LeftCancelSemigroup.ext {G : Type u} {x y : LeftCancelSemigroup G} (mul : Mul.mul = Mul.mul) :
x = y
source
def Mathlib.LibraryNote.«lower cancel priority» :
LibraryNote

We lower the priority of inheriting from cancellative structures. This attempts to avoid expensive checks involving bundling and unbundling with the `IsDomain` class. since `IsDomain` already depends on `Semiring`, we can synthesize that one first. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Why.20is.20.60simpNF.60.20complaining.20here.3F

Equations

- Mathlib.LibraryNote.«lower cancel priority» = ()

Instances For

source
class AddLeftCancelSemigroup (G : Type u) extends AddSemigroup G, IsLeftCancelAdd G :
Type u

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

- add : G → G → G
- add_assoc (a b c : G) : a + b + c = a + (b + c)
- add_left_cancel (a : G) : IsAddLeftRegular a

Instances

source
theorem AddLeftCancelSemigroup.ext {G : Type u} {x y : AddLeftCancelSemigroup G} (add : Add.add = Add.add) :
x = y
source
theorem AddLeftCancelSemigroup.ext_iff {G : Type u} {x y : AddLeftCancelSemigroup G} :
x = y ↔ Add.add = Add.add
source
class RightCancelSemigroup (G : Type u) extends Semigroup G, IsRightCancelMul G :
Type u

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

- mul : G → G → G
- mul_assoc (a b c : G) : a * b * c = a * (b * c)
- mul_right_cancel (a : G) : IsRightRegular a

Instances

source
theorem RightCancelSemigroup.ext {G : Type u} {x y : RightCancelSemigroup G} (mul : Mul.mul = Mul.mul) :
x = y
source
theorem RightCancelSemigroup.ext_iff {G : Type u} {x y : RightCancelSemigroup G} :
x = y ↔ Mul.mul = Mul.mul
source
class AddRightCancelSemigroup (G : Type u) extends AddSemigroup G, IsRightCancelAdd G :
Type u

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

- add : G → G → G
- add_assoc (a b c : G) : a + b + c = a + (b + c)
- add_right_cancel (a : G) : IsAddRightRegular a

Instances

source
theorem AddRightCancelSemigroup.ext {G : Type u} {x y : AddRightCancelSemigroup G} (add : Add.add = Add.add) :
x = y
source
theorem AddRightCancelSemigroup.ext_iff {G : Type u} {x y : AddRightCancelSemigroup G} :
x = y ↔ Add.add = Add.add
source
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

Instances

source
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

Instances

source
theorem MulOne.ext {M : Type u_2} {x y : MulOne M} (one : One.one = One.one) (mul : Mul.mul = Mul.mul) :
x = y
source
theorem MulOne.ext_iff {M : Type u_2} {x y : MulOne M} :
x = y ↔ One.one = One.one ∧ Mul.mul = Mul.mul
source
class AddZeroClass (M : Type u) extends AddZero M :
Type u

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

Instances

source
class MulOneClass (M : Type u) extends MulOne M :
Type u

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

Instances

source
theorem MulOneClass.ext {M : Type u} ⦃m₁ m₂ : MulOneClass M⦄ :
Mul.mul = Mul.mul → m₁ = m₂
source
theorem AddZeroClass.ext {M : Type u} ⦃m₁ m₂ : AddZeroClass M⦄ :
Add.add = Add.add → m₁ = m₂
source
theorem MulOneClass.ext_iff {M : Type u} {m₁ m₂ : MulOneClass M} :
m₁ = m₂ ↔ Mul.mul = Mul.mul
source
theorem AddZeroClass.ext_iff {M : Type u} {m₁ m₂ : AddZeroClass M} :
m₁ = m₂ ↔ Add.add = Add.add
source
@[simp]
theorem one_mul {M : Type u} [MulOneClass M] (a : M) :
1 * a = a
source
@[simp]
theorem zero_add {M : Type u} [AddZeroClass M] (a : M) :
0 + a = a
source
@[simp]
theorem mul_one {M : Type u} [MulOneClass M] (a : M) :
a * 1 = a
source
@[simp]
theorem add_zero {M : Type u} [AddZeroClass M] (a : M) :
a + 0 = a
source
theorem npowRec_add {M : Type u} [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
source
theorem nsmulRec_add {M : Type u} [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
source
theorem npowRec_succ {M : Type u} [One M] [Semigroup M] (n : ℕ) (hn : n ≠ 0) (a : M) (ha : 1 * a = a) :
npowRec (n + 1) a = a * npowRec n a
source
theorem nsmulRec_succ {M : Type u} [Zero M] [AddSemigroup M] (n : ℕ) (hn : n ≠ 0) (a : M) (ha : 0 + a = a) :
nsmulRec (n + 1) a = a + nsmulRec n a
source
def Mathlib.LibraryNote.«forgetful inheritance» :
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

- Mathlib.LibraryNote.«forgetful inheritance» = ()

Instances For

### 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.

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

Exponentiation by repeated squaring.

Equations

- npowBinRec k = npowBinRec.go k 1

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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✝

Instances For

source
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✝

Instances For

source
theorem npowRec'_succ {M : Type u_2} [Mul M] [One M] {k : ℕ} :
k ≠ 0 → ∀ (m : M), npowRec' (k + 1) m = npowRec' k m * m
source
theorem nsmulRec'_succ {M : Type u_2} [Add M] [Zero M] {k : ℕ} :
k ≠ 0 → ∀ (m : M), nsmulRec' (k + 1) m = nsmulRec' k m + m
source
theorem npowRec'_two_mul {M : Type u_2} [Semigroup M] [One M] (k : ℕ) (m : M) :
npowRec' (2 * k) m = npowRec' k (m * m)
source
theorem nsmulRec'_two_add {M : Type u_2} [AddSemigroup M] [Zero M] (k : ℕ) (m : M) :
nsmulRec' (2 * k) m = nsmulRec' k (m + m)
source
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
source
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
source
theorem npowRec_eq {M : Type u_2} [Semigroup M] [One M] (k : ℕ) (m : M) :
npowRec (k + 1) m = 1 * npowRec' (k + 1) m
source
theorem nsmulRec_eq {M : Type u_2} [AddSemigroup M] [Zero M] (k : ℕ) (m : M) :
nsmulRec (k + 1) m = 0 + nsmulRec' (k + 1) m
source
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
source
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
source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[csimp]
theorem npowRec_eq_npowBinRec :
@npowRecAuto = @npowBinRecAuto
source
@[csimp]
theorem nsmulRec_eq_nsmulBinRec :
@nsmulRecAuto = @nsmulBinRecAuto
source
class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M :
Type u

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

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

- nsmul_zero (x : M) : AddMonoid.nsmul 0 x = 0

  Multiplication by `(0 : ℕ)` gives `0`.

- nsmul_succ (n : ℕ) (x : M) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

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

Instances

source
class Monoid (M : Type u) extends Semigroup M, MulOneClass M :
Type u

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

  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 = Monoid.npow n x * x

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

Instances

source
@[defaultInstance 10000]
instance Monoid.toNatPow {M : Type u_2} [Monoid M] :
Pow M ℕ
Equations

- Monoid.toNatPow = { pow := fun (x : M) (n : ℕ) => Monoid.npow n x }

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

- AddMonoid.toNatSMul = { smul := AddMonoid.nsmul }

source
@[simp]
theorem npow_eq_pow {M : Type u_2} [Monoid M] (n : ℕ) (x : M) :
Monoid.npow n x = x ^ n
source
@[simp]
theorem nsmul_eq_smul {M : Type u_2} [AddMonoid M] (n : ℕ) (x : M) :
AddMonoid.nsmul n x = n • x
source
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
source
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
source
@[simp]
theorem pow_zero {M : Type u_2} [Monoid M] (a : M) :
a ^ 0 = 1
source
@[simp]
theorem zero_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
0 • a = 0
source
theorem pow_succ {M : Type u_2} [Monoid M] (a : M) (n : ℕ) :
a ^ (n + 1) = a ^ n * a
source
theorem succ_nsmul {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) :
(n + 1) • a = n • a + a
source
@[simp]
theorem pow_one {M : Type u_2} [Monoid M] (a : M) :
a ^ 1 = a
source
@[simp]
theorem one_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
1 • a = a
source
theorem pow_succ' {M : Type u_2} [Monoid M] (a : M) (n : ℕ) :
a ^ (n + 1) = a * a ^ n
source
theorem succ_nsmul' {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) :
(n + 1) • a = a + n • a
source
theorem mul_pow_mul {M : Type u_2} [Monoid M] (a b : M) (n : ℕ) :
(a * b) ^ n * a = a * (b * a) ^ n
source
theorem add_nsmul_add {M : Type u_2} [AddMonoid M] (a b : M) (n : ℕ) :
n • (a + b) + a = a + n • (b + a)
source
theorem pow_mul_comm' {M : Type u_2} [Monoid M] (a : M) (n : ℕ) :
a ^ n * a = a * a ^ n
source
theorem nsmul_add_comm' {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) :
n • a + a = a + n • a
source
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`.

source
theorem two_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
2 • a = a + a
source
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`.

source
theorem pow_three' {M : Type u_2} [Monoid M] (a : M) :
a ^ 3 = a * a * a
source
theorem three'_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
3 • a = a + a + a
source
theorem pow_three {M : Type u_2} [Monoid M] (a : M) :
a ^ 3 = a * (a * a)
source
theorem three_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
3 • a = a + (a + a)
source
@[simp]
theorem one_pow {M : Type u_2} [Monoid M] (n : ℕ) :
1 ^ n = 1
source
@[simp]
theorem nsmul_zero {M : Type u_2} [AddMonoid M] (n : ℕ) :
n • 0 = 0
source
theorem pow_add {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) :
a ^ (m + n) = a ^ m * a ^ n
source
theorem add_nsmul {M : Type u_2} [AddMonoid M] (a : M) (m n : ℕ) :
(m + n) • a = m • a + n • a
source
theorem pow_mul_comm {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) :
a ^ m * a ^ n = a ^ n * a ^ m
source
theorem nsmul_add_comm {M : Type u_2} [AddMonoid M] (a : M) (m n : ℕ) :
m • a + n • a = n • a + m • a
source
theorem pow_mul {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) :
a ^ (m * n) = (a ^ m) ^ n
source
theorem mul_nsmul {M : Type u_2} [AddMonoid M] (a : M) (m n : ℕ) :
(m * n) • a = n • m • a
source
theorem pow_mul' {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) :
a ^ (m * n) = (a ^ n) ^ m
source
theorem mul_nsmul' {M : Type u_2} [AddMonoid M] (a : M) (m n : ℕ) :
(m * n) • a = m • n • a
source
theorem pow_right_comm {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) :
(a ^ m) ^ n = (a ^ n) ^ m
source
theorem nsmul_left_comm {M : Type u_2} [AddMonoid M] (a : M) (m n : ℕ) :
n • m • a = m • n • a
source
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

Instances

source
theorem isAddTorsionFree_iff (M : Type u_2) [AddMonoid M] :
IsAddTorsionFree M ↔ ∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun (a : M) => n • a
source
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

Instances

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

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

Instances

source
class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M :
Type u

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

Instances

source
class AddLeftCancelMonoid (M : Type u) extends AddMonoid M, AddLeftCancelSemigroup M :
Type u

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

Instances

source
class LeftCancelMonoid (M : Type u) extends Monoid M, LeftCancelSemigroup M :
Type u

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

Instances

source
class AddRightCancelMonoid (M : Type u) extends AddMonoid M, AddRightCancelSemigroup M :
Type u

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

Instances

source
class RightCancelMonoid (M : Type u) extends Monoid M, RightCancelSemigroup M :
Type u

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

Instances

source
class AddCancelMonoid (M : Type u) extends AddLeftCancelMonoid M, AddRightCancelMonoid M :
Type u

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

Instances

source
class CancelMonoid (M : Type u) extends LeftCancelMonoid M, RightCancelMonoid M :
Type u

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

Instances

source
class AddCancelCommMonoid (M : Type u) extends AddCommMonoid M, AddLeftCancelMonoid M :
Type u

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

Instances

source
class CancelCommMonoid (M : Type u) extends CommMonoid M, LeftCancelMonoid M :
Type u

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

Instances

source
@[instance 100]
instance CancelCommMonoid.toCancelMonoid (M : Type u) [CancelCommMonoid M] :
CancelMonoid M
Equations

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

source
@[instance 100]
instance AddCancelCommMonoid.toAddCancelMonoid (M : Type u) [AddCancelCommMonoid M] :
AddCancelMonoid M
Equations

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

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

Any `CancelMonoid G` satisfies `IsCancelMul G`.

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

Any `AddCancelMonoid G` satisfies `IsCancelAdd G`.

source
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.

Equations

- zpowRec npow (Int.ofNat n) x✝ = npow n x✝
- zpowRec npow (Int.negSucc n) x✝ = (npow n.succ x✝)⁻¹

Instances For

source
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.

Equations

- zsmulRec nsmul (Int.ofNat n) x✝ = nsmul n x✝
- zsmulRec nsmul (Int.negSucc n) x✝ = -nsmul n.succ x✝

Instances For

source
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

Instances

source
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

Instances

source
@[simp]
theorem inv_inv {G : Type u_1} [InvolutiveInv G] (a : G) :
a⁻¹⁻¹ = a
source
@[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`.

source
def DivInvMonoid.div' {G : Type u} [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 `DivInvMonoid`s constructed using that default value will not be unfolded at `.instance` transparency.

Equations

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

Instances For

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

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.

- 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 = Monoid.npow n x * 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 (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a

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

- zpow_neg' (n : ℕ) (a : G) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹

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

Instances

source
def SubNegMonoid.sub' {G : Type u} [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 `SubNegMonoid`s constructed using that default value will not be unfolded at `.instance` transparency.

Equations

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

Instances For

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

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.

- 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 = AddMonoid.nsmul n x + x
- neg : G → G
- sub : G → G → G
- sub_eq_add_neg (a b : G) : a - b = a + -b
- zsmul : ℤ → G → G

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

- zsmul_zero' (a : G) : SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' (n : ℕ) (a : G) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' (n : ℕ) (a : G) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a

Instances

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

- DivInvMonoid.toZPow = { pow := fun (x : M) (n : ℤ) => DivInvMonoid.zpow n x }

source
instance SubNegMonoid.toZSMul {M : Type u_2} [SubNegMonoid M] :
SMul ℤ M
Equations

- SubNegMonoid.toZSMul = { smul := SubNegMonoid.zsmul }

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

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

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

Instances

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

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

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

Instances

source
theorem exists_zpow_surjective (G : Type u_2) [Pow G ℤ] [IsCyclic G] :
∃ (g : G), Function.Surjective fun (x : ℤ) => g ^ x
source
theorem exists_zsmul_surjective (G : Type u_2) [SMul ℤ G] [IsAddCyclic G] :
∃ (g : G), Function.Surjective fun (x : ℤ) => x • g
source
@[simp]
theorem zpow_eq_pow {G : Type u_1} [DivInvMonoid G] (n : ℤ) (x : G) :
DivInvMonoid.zpow n x = x ^ n
source
@[simp]
theorem zsmul_eq_smul {G : Type u_1} [SubNegMonoid G] (n : ℤ) (x : G) :
SubNegMonoid.zsmul n x = n • x
source
@[simp]
theorem zpow_zero {G : Type u_1} [DivInvMonoid G] (a : G) :
a ^ 0 = 1
source
@[simp]
theorem zero_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) :
0 • a = 0
source
@[simp]
theorem zpow_natCast {G : Type u_1} [DivInvMonoid G] (a : G) (n : ℕ) :
a ^ ↑n = a ^ n
source
@[simp]
theorem natCast_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) (n : ℕ) :
↑n • a = n • a
source
theorem zpow_ofNat {G : Type u_1} [DivInvMonoid G] (a : G) (n : ℕ) :
a ^ OfNat.ofNat n = a ^ OfNat.ofNat n
source
theorem ofNat_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) (n : ℕ) :
OfNat.ofNat n • a = OfNat.ofNat n • a
source
@[simp]
theorem zpow_negSucc {G : Type u_1} [DivInvMonoid G] (a : G) (n : ℕ) :
a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
source
@[simp]
theorem negSucc_zsmul {G : Type u_2} [SubNegMonoid G] (a : G) (n : ℕ) :
Int.negSucc n • a = -((n + 1) • a)
source
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.

source
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.

source
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.

source
theorem inv_eq_one_div {G : Type u_1} [DivInvMonoid G] (x : G) :
x⁻¹ = 1 / x
source
theorem neg_eq_zero_sub {G : Type u_1} [SubNegMonoid G] (x : G) :
-x = 0 - x
source
theorem mul_div_assoc {G : Type u_1} [DivInvMonoid G] (a b c : G) :
a * b / c = a * (b / c)
source
theorem add_sub_assoc {G : Type u_1} [SubNegMonoid G] (a b c : G) :
a + b - c = a + (b - c)
source
@[simp]
theorem one_div {G : Type u_1} [DivInvMonoid G] (a : G) :
1 / a = a⁻¹
source
@[simp]
theorem zero_sub {G : Type u_1} [SubNegMonoid G] (a : G) :
0 - a = -a
source
@[simp]
theorem zpow_one {G : Type u_1} [DivInvMonoid G] (a : G) :
a ^ 1 = a
source
@[simp]
theorem one_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) :
1 • a = a
source
theorem zpow_two {G : Type u_1} [DivInvMonoid G] (a : G) :
a ^ 2 = a * a
source
theorem two_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) :
2 • a = a + a
source
theorem zpow_neg_one {G : Type u_1} [DivInvMonoid G] (x : G) :
x ^ (-1) = x⁻¹
source
theorem neg_one_zsmul {G : Type u_1} [SubNegMonoid G] (x : G) :
-1 • x = -x
source
theorem zpow_neg_coe_of_pos {G : Type u_1} [DivInvMonoid G] (a : G) {n : ℕ} :
0 < n → a ^ (-↑n) = (a ^ n)⁻¹
source
theorem zsmul_neg_coe_of_pos {G : Type u_1} [SubNegMonoid G] (a : G) {n : ℕ} :
0 < n → -↑n • a = -(n • a)
source
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

Instances

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

A `SubNegMonoid` where `-0 = 0`.

- 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 = AddMonoid.nsmul n x + 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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' (n : ℕ) (a : G) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_zero : -0 = 0

Instances

source
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

Instances

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

A `DivInvMonoid` where `1⁻¹ = 1`.

- 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 = Monoid.npow n x * 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 (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' (n : ℕ) (a : G) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
- inv_one : 1⁻¹ = 1

Instances

source
@[simp]
theorem inv_one {G : Type u_1} [InvOneClass G] :
1⁻¹ = 1
source
@[simp]
theorem neg_zero {G : Type u_1} [NegZeroClass G] :
-0 = 0
source
class SubtractionMonoid (G : Type u) extends SubNegMonoid G, InvolutiveNeg G :
Type u

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

- 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 = AddMonoid.nsmul n x + 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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' (n : ℕ) (a : G) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑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.

Instances

source
class DivisionMonoid (G : Type u) extends DivInvMonoid G, InvolutiveInv G :
Type u

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`.

- 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 = Monoid.npow n x * 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 (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' (n : ℕ) (a : G) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) 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

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

Instances

source
@[simp]
theorem mul_inv_rev {G : Type u_1} [DivisionMonoid G] (a b : G) :
(a * b)⁻¹ = b⁻¹ * a⁻¹
source
@[simp]
theorem neg_add_rev {G : Type u_1} [SubtractionMonoid G] (a b : G) :
-(a + b) = -b + -a
source
theorem inv_eq_of_mul_eq_one_right {G : Type u_1} [DivisionMonoid G] {a b : G} :
a * b = 1 → a⁻¹ = b
source
theorem neg_eq_of_add_eq_zero_right {G : Type u_1} [SubtractionMonoid G] {a b : G} :
a + b = 0 → -a = b
source
theorem inv_eq_of_mul_eq_one_left {G : Type u_1} [DivisionMonoid G] {a b : G} (h : a * b = 1) :
b⁻¹ = a
source
theorem neg_eq_of_add_eq_zero_left {G : Type u_1} [SubtractionMonoid G] {a b : G} (h : a + b = 0) :
-b = a
source
theorem eq_inv_of_mul_eq_one_left {G : Type u_1} [DivisionMonoid G] {a b : G} (h : a * b = 1) :
a = b⁻¹
source
theorem eq_neg_of_add_eq_zero_left {G : Type u_1} [SubtractionMonoid G] {a b : G} (h : a + b = 0) :
a = -b
source
class SubtractionCommMonoid (G : Type u) extends SubtractionMonoid G, AddCommMonoid G :
Type u

Commutative `SubtractionMonoid`.

- 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 = AddMonoid.nsmul n x + 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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' (n : ℕ) (a : G) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑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

Instances

source
class DivisionCommMonoid (G : Type u) extends DivisionMonoid G, CommMonoid G :
Type u

Commutative `DivisionMonoid`.

This is the immediate common ancestor of `CommGroup` and `CommGroupWithZero`.

- 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 = Monoid.npow n x * 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 (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' (n : ℕ) (a : G) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) 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

Instances

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

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

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

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

- 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 = Monoid.npow n x * 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 (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' (n : ℕ) (a : G) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
- inv_mul_cancel (a : G) : a⁻¹ * a = 1

Instances

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

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

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

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

- 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 = AddMonoid.nsmul n x + 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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' (n : ℕ) (a : A) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_add_cancel (a : A) : -a + a = 0

Instances

source
@[simp]
theorem inv_mul_cancel {G : Type u_1} [Group G] (a : G) :
a⁻¹ * a = 1
source
@[simp]
theorem neg_add_cancel {G : Type u_1} [AddGroup G] (a : G) :
-a + a = 0
source
@[simp]
theorem mul_inv_cancel {G : Type u_1} [Group G] (a : G) :
a * a⁻¹ = 1
source
@[simp]
theorem add_neg_cancel {G : Type u_1} [AddGroup G] (a : G) :
a + -a = 0
source
@[simp]
theorem div_self' {G : Type u_1} [Group G] (a : G) :
a / a = 1
source
@[simp]
theorem sub_self {G : Type u_1} [AddGroup G] (a : G) :
a - a = 0
source
@[simp]
theorem inv_mul_cancel_left {G : Type u_1} [Group G] (a b : G) :
a⁻¹ * (a * b) = b
source
@[simp]
theorem neg_add_cancel_left {G : Type u_1} [AddGroup G] (a b : G) :
-a + (a + b) = b
source
@[simp]
theorem mul_inv_cancel_left {G : Type u_1} [Group G] (a b : G) :
a * (a⁻¹ * b) = b
source
@[simp]
theorem add_neg_cancel_left {G : Type u_1} [AddGroup G] (a b : G) :
a + (-a + b) = b
source
@[simp]
theorem mul_inv_cancel_right {G : Type u_1} [Group G] (a b : G) :
a * b * b⁻¹ = a
source
@[simp]
theorem add_neg_cancel_right {G : Type u_1} [AddGroup G] (a b : G) :
a + b + -b = a
source
@[simp]
theorem mul_div_cancel_right {G : Type u_1} [Group G] (a b : G) :
a * b / b = a
source
@[simp]
theorem add_sub_cancel_right {G : Type u_1} [AddGroup G] (a b : G) :
a + b - b = a
source
@[simp]
theorem inv_mul_cancel_right {G : Type u_1} [Group G] (a b : G) :
a * b⁻¹ * b = a
source
@[simp]
theorem neg_add_cancel_right {G : Type u_1} [AddGroup G] (a b : G) :
a + -b + b = a
source
@[simp]
theorem div_mul_cancel {G : Type u_1} [Group G] (a b : G) :
a / b * b = a
source
@[simp]
theorem sub_add_cancel {G : Type u_1} [AddGroup G] (a b : G) :
a - b + b = a
source
@[instance 100]
instance Group.toDivisionMonoid {G : Type u_1} [Group G] :
DivisionMonoid G
Equations

- Group.toDivisionMonoid = { toDivInvMonoid := inst✝.toDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }

source
@[instance 100]
instance AddGroup.toSubtractionMonoid {G : Type u_1} [AddGroup G] :
SubtractionMonoid G
Equations

- AddGroup.toSubtractionMonoid = { toSubNegMonoid := inst✝.toSubNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }

source
@[instance 100]
instance Group.toCancelMonoid {G : Type u_1} [Group G] :
CancelMonoid G
Equations

- Group.toCancelMonoid = { toMonoid := inst✝.toMonoid, toIsLeftCancelMul := ⋯, toIsRightCancelMul := ⋯ }

source
@[instance 100]
instance AddGroup.toAddCancelMonoid {G : Type u_1} [AddGroup G] :
AddCancelMonoid G
Equations

- AddGroup.toAddCancelMonoid = { toAddMonoid := inst✝.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }

source
class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G :
Type u

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

- 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 = AddMonoid.nsmul n x + 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 (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' (n : ℕ) (a : G) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_add_cancel (a : G) : -a + a = 0
- add_comm (a b : G) : a + b = b + a

Instances

source
class CommGroup (G : Type u) extends Group G, CommMonoid G :
Type u

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

- 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 = Monoid.npow n x * 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 (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' (n : ℕ) (a : G) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
- inv_mul_cancel (a : G) : a⁻¹ * a = 1
- mul_comm (a b : G) : a * b = b * a

Instances

source
@[instance 100]
instance CommGroup.toCancelCommMonoid {G : Type u_1} [CommGroup G] :
CancelCommMonoid G
Equations

- CommGroup.toCancelCommMonoid = { toMonoid := inst✝.toMonoid, mul_comm := ⋯, toIsLeftCancelMul := ⋯ }

source
@[instance 100]
instance AddCommGroup.toAddCancelCommMonoid {G : Type u_1} [AddCommGroup G] :
AddCancelCommMonoid G
Equations

- AddCommGroup.toAddCancelCommMonoid = { toAddMonoid := inst✝.toAddMonoid, add_comm := ⋯, toIsLeftCancelAdd := ⋯ }

source
@[instance 100]
instance CommGroup.toDivisionCommMonoid {G : Type u_1} [CommGroup G] :
DivisionCommMonoid G
Equations

- CommGroup.toDivisionCommMonoid = { toDivInvMonoid := inst✝.toDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯, mul_comm := ⋯ }

source
@[instance 100]
instance AddCommGroup.toDivisionAddCommMonoid {G : Type u_1} [AddCommGroup G] :
SubtractionCommMonoid G
Equations

- AddCommGroup.toDivisionAddCommMonoid = { toSubNegMonoid := inst✝.toSubNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯, add_comm := ⋯ }

source
@[simp]
theorem inv_mul_cancel_comm {G : Type u_1} [CommGroup G] (a b : G) :
a⁻¹ * b * a = b
source
@[simp]
theorem neg_add_cancel_comm {G : Type u_1} [AddCommGroup G] (a b : G) :
-a + b + a = b
source
@[simp]
theorem mul_inv_cancel_comm {G : Type u_1} [CommGroup G] (a b : G) :
a * b * a⁻¹ = b
source
@[simp]
theorem add_neg_cancel_comm {G : Type u_1} [AddCommGroup G] (a b : G) :
a + b + -a = b
source
@[simp]
theorem inv_mul_cancel_comm_assoc {G : Type u_1} [CommGroup G] (a b : G) :
a⁻¹ * (b * a) = b
source
@[simp]
theorem neg_add_cancel_comm_assoc {G : Type u_1} [AddCommGroup G] (a b : G) :
-a + (b + a) = b
source
@[simp]
theorem mul_inv_cancel_comm_assoc {G : Type u_1} [CommGroup G] (a b : G) :
a * (b * a⁻¹) = b
source
@[simp]
theorem add_neg_cancel_comm_assoc {G : Type u_1} [AddCommGroup G] (a b : G) :
a + (b + -a) = b
source
class IsAddCommutative (M : Type u_2) [Add M] :
Prop

A Prop stating that the addition is commutative.

- is_comm : Std.Commutative fun (x1 x2 : M) => x1 + x2

Instances

source
class IsMulCommutative (M : Type u_2) [Mul M] :
Prop

A Prop stating that the multiplication is commutative.

- is_comm : Std.Commutative fun (x1 x2 : M) => x1 * x2

Instances

source
@[instance 100]
instance CommMonoid.ofIsMulCommutative {M : Type u_2} [Monoid M] [IsMulCommutative M] :
CommMonoid M
Equations

- CommMonoid.ofIsMulCommutative = { toMonoid := inst✝¹, mul_comm := ⋯ }

source
@[instance 100]
instance AddCommMonoid.ofIsAddCommutative {M : Type u_2} [AddMonoid M] [IsAddCommutative M] :
AddCommMonoid M
Equations

- AddCommMonoid.ofIsAddCommutative = { toAddMonoid := inst✝¹, add_comm := ⋯ }

source
@[instance 100]
instance CommGroup.ofIsMulCommutative {G : Type u_2} [Group G] [IsMulCommutative G] :
CommGroup G
Equations

- CommGroup.ofIsMulCommutative = { toGroup := inst✝¹, mul_comm := ⋯ }

source
@[instance 100]
instance AddCommGroup.ofIsAddCommutative {G : Type u_2} [AddGroup G] [IsAddCommutative G] :
AddCommGroup G
Equations

- AddCommGroup.ofIsAddCommutative = { toAddGroup := inst✝¹, add_comm := ⋯ }

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.