# Lecture 4.2: Mathematics — Algebra

Central to nearly everything in mathematics is algebra

Today we introduce definitions and proofs about basic mathematical structures


## `mathlib`

Lean's core library includes only basic algebraic definitions

More setup and especially tactics are found in [mathlib](https://github.com/leanprover/mathlib/): Lean's mathematical library


## Syntactic classes

We start with "syntactic" type classes, which contain constants but no assumptions:

    class has_mul (α : Type) := (mul : α → α → α)
    class has_one (α : Type) := (one : α)
    class has_inv (α : Type) := (inv : α → α)

For these type classes, the traditional symbols `*`, `1`, and `⁻¹` are defined in Lean's core library (`library/init/core.lean`)

The "semantic" hierarchy is build on top of the syntactic type classes


## Classes over a single binary operator

Many of the following structures are very simple, but provide a long list of derived facts and constants building on them (e.g. big operators)

Lean starts the algebraic hierarchy with one binary operator, called `*`:

Structure                | Properties
------------------------ | ------------
`semigroup`              | associativity
`monoid`                 | `semigroup` with unit (`1`)
`group`                  | `monoid` with inverse (`⁻¹`)
`left_cancel_semigroup`  | `semigroup` with `x * a = x * b → a = b`
`right_cancel_semigroup` | `semigroup` with `a * x = b * x → a = b`

Most of these structures have commutative versions, prefixed with `comm_`:

    comm_semigroup, comm_monoid, comm_group

The _multiplicative_ structures (over `*`, `1`, `⁻¹`) are copied to produce _additive_ versions (over `+`, `0`, `-`), prefixed with `add_`

The copying process is automated by the `transport_multiplicative_to_additive` tactic and the `to_additive` attribute provided by `mathlib`

    add_semigroup, add_monoid, add_group
    add_comm_semigroup, add_comm_monoid, add_comm_group,
    add_left_cancel_semigroup, add_right_cancel_semigroup

Example instance for `add_monoid`: `list` with `++` and `[]` (which is also a `add_left_cancel_semigroup` and a `add_right_cancel_semigroup`)

![Hierarchy](hierarchy.png)

## Rings and fields

The additive and multiplicative structures are combined to form rings and fields

The commutative versions assume commutativity of `*`

Structure       | Comm. version    | Properties                                        | Instances
--------------- | ---------------- | ------------------------------------------------- | ---
`semiring`      | `comm_semiring`  | `monoid`, `add_comm_monoid` with distributivity   | `ℕ` and all rings
`ring`          | `comm_ring`      | `monoid`, `add_comm_group` with distributivity    | `ℤ` and all fields
`division_ring` | `field`          | `ring` with multiplicative inverse                | `ℚ` and `ℝ`

By convention, `∀n, n / 0 = 0` in `discrete_field`

The hierarchy between `ring` and `field` is more fine-grained: (integral) domains, Euclidean rings, etc.


## Ordered structures

Type classes combining orders and algebraic structures are also available:

    ordered_cancel_comm_monoid, ordered_comm_group
    ordered_semiring, linear_ordered_semiring, linear_ordered_comm_ring
    linear_ordered_field

All these mathematical structures relate `≤` and `<` with the constants `0`, `1`, `+`, and `*` by monotonicity rules `a ≤ b → c ≤ d → a + c ≤ b + d` and cancellation rules `x + b ≤ x + c → b ≤ c`


## Big operators

Big operators (∑ and ∏) allow us to sum (or multiply) a family of values

    a1 + a2 + ... + aN

`mathlib` provides `prod` and `sum` operations over `list` (ordered, with duplicates), `multiset` (unordered, with duplicates), and `finset` (unordered, no duplicates)

The big operators `list.prod`, `multiset.prod`, and `finset.prod` are first introduced and then copied using the `to_additive` attribute

Big operators over `list`s for `add_monoid`:

    list.sum []       = 0
    list.sum (a :: l) = a + list.sum l

Big operators over `multiset`s for `add_comm_monoid`:

    multiset.sum ∅        = 0
    multiset.sum {a}      = a
    multiset.sum (a :: m) = a + multiset.sum m
    multiset.sum (s ∪ t)  = multiset.sum s + multiset.sum t

Big operators over `finset`s for `add_comm_monoid`:

    finset.sum f ∅            = 0
    finset.sum f {a}          = f a
    finset.sum f (insert a s) = f a + finset.sum f s               if a ∉ s
    finset.sum f (s ∪ t)      = finset.sum f s + finset.sum f t    if s ∩ t = ∅

Notice the presence of an indexed-family `f`

`mathlib` provides a collections of lemmas describing how the big operators behave under reorderings, basic operators on `list`, `multiset`, and `finset`, morphisms, order relations, and more


## Coercions

In mathematics, we have subset relations between different "types" of numbers:

    ℕ ⊆ ℤ ⊆ ℚ ⊆ ℝ

In Lean, each is represented by its own type, with injective morphisms representing the subsets

Lean's **coercion mechanism** is set up to introduce these morphisms automatically, to lighten notation

The coercion operator is `coe` (written `↑`) and can be setup to convert arbitrary types

For numbers we have

* `coe : ℕ → α` for a semiring `α`, which allows us to embed `ℕ` into another semiring

* `coe : ℤ → α` for a ring `α`, which allows us to embed `ℤ` into another ring

* `coe : ℚ → α` for a division ring `α`, which allows us to embed `ℚ` into another division ring

All of these coercions support the desirable morphism laws:

    ↑0       = 0
    ↑1       = 1
    ↑(a + b) = ↑a + ↑b
    ↑(a * b) = ↑a * ↑b
    ↑a ≤ ↑b  ↔ a ≤ b


## Numerals

Number literals are represented as sequences of `bit0` and `bit1`:

* `0`, `1`, `bit0 n := n + n`, `bit1 n := n + n + 1`

* `16` = `bit0 (bit0 (bit0 (bit0 1)))`


## Tactics

### `ac_refl`

Reflexivity modulo associativity and commutativity (`is_associative` and `is_commutative` type classes)

### `ring` and `abel`

Normalizes ring terms or terms of commutative monoids and groups

### `norm_num`

Normalizes numerals (`dec_trivial` only works for `ℕ`)

### `linarith`

Decides linear arithmetic problems (e.g. `10 < 5 + 13 * x + 17 * y`)


## Demo

[`42_lecture.lean`](42_lecture.lean)


## Newly introduced syntax

### Tactics

Name         | Description
------------ | -----------
`abel`       | normalizes terms of commutative monoids and groups
`linarith`   | decides linear arithmetic problems
`norm_num`   | normalizes numerals
`ring`       | normalizes ring terms


## References

* [_Theorem Proving in Lean_](https://leanprover.github.io/theorem_proving_in_lean/) by Jeremy Avigad et al., Section 6.7
