# 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: 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
``````

Example instance for `add_monoid`: `list` with `++` and `[]` (which is also a `add_left_cancel_semigroup` and a `add_right_cancel_semigroup`) ## 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`

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