In this document, we unify the informal mathematical language for a definition to:

\optional{Let \placeholder{\(X\)} be a \placeholder{\vocab{concept \(X\)}}. }

A \newvocab{\placeholder{concept \(Z\)}} is a set/pair/triple/tuple \((Z, \mathtt {op}, ...)\), satisfying:

1. \placeholder{\(Z\)} is a \placeholder{\vocab{concept \(Y\)}} \optional{ over \placeholder{\(X\)} under \placeholder{op} }.
2. \placeholder{formula} for all \placeholder{elements in \(Z\)} \optional{(\vocab{ \placeholder{property} })}.
3. \optional{for each \placeholder{element} in \placeholder{\vocab{concept \(X\)}}, } there exists \placeholder{element} such that \placeholder{formula} for all \placeholder{elements in concept \(Z\)}.
4. \optional{\placeholder{op} is called \placeholder{\vocab{op name}}, }for all \placeholder{elements in \(Z\)}, we have
   1. \placeholder{formula}
   2. \placeholder{formula}
   \optional{(\vocab{ \placeholder{property} })}.

By default, \placeholder{\(X\)} is a set, \placeholder{op} is a binary operation on \placeholder{\(X\)}.

A group is a pair \((G, *)\), satisfying:

1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in G\) (associativity).
2. there exists \(1 \in G\) such that \[1 * a = a * 1 = a\] for all \(a \in G\).
3. for each \(a \in G\), there exists \(a^{-1} \in G\) such that \[a * a^{-1} = a^{-1} * a = 1\].

It then follows that \(1\), the identity element, is unique, and that for each \(g \in G\) the inverse \(g^{-1}\) is unique. A group G is abelian, or commutative, if \(g * h = h * g\) for all \(g, h \in G\).

In literatures, the binary operation of a group is usually called a product. It's denoted by juxtaposition \(g h\), and is understood to be a mapping \((g, h) \mapsto g * h\) from \(G \times G\) to \(G\).

Here we use an explicit symbol for the operation. It can be denoted multiplicatively as \(*\) in Group or additively as \(+\) in AddGroup, where the identity element will be denoted by \(1\) or \(0\), respectively.

Sometimes we use notations with subscripts (e.g. \(*_G\), \(1_G\)) to indicate where they are.

\(\textsf {Mathlib}\) encodes the mapping \(G \times G \to G\) as \(G \to G \to G\), it is understood to be \(G \to (G \to G)\), that sends \(g \in G\) to a mapping that sends \(h \in G\) to \(g * h \in G\).

Furthermore, a mathematical construct, e.g. a group, is represented by a "type", as Lean has a dependent type theory foundation, see [carneiro2019type] and [ullrich2023extensible, sec. 3.2].

A monoid is a pair \((R, *)\), satisfying:

1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in R\) (associativity).
2. there exists an element \(1 \in R\) such that \(1 * a = a * 1 = a\) for all \(a \in R\)
i.e. \(1\) is the multiplicative identity (neutral element).

A ring is a triple \((R, +, *)\), satisfying:

1. \(R\) is a commutative group under \(+\).
2. \(R\) is a monoid under \(*\).
3. for all \(a, b, c \in R\), we have
   1. \(a * (b + c) = a * b + a * c\)
   2. \((a + b) * c = a * c + b * c\)
   (left and right distributivity over \(+\)).

In applications to Clifford algebras \(R\) will be always assumed to be commutative.

A division ring is a ring \((R, +, *)\), satisfying:

1. \(R\) contains at least 2 elements.
2. for all \(a \neq 0\) in \(R\), there exists a multiplicative inverse \(a^{-1} \in R\) such that
\[ a * a^{-1} = a^{-1} * a = 1 \]

Let \(R\) be a commutative ring. A module over \(R\), called an \(R\)-module, is a pair \((M, \bullet )\), satisfying:

1. M is a group under \(+\).
2. \(\bullet : R \to M \to M\) is called scalar multiplication, for every \(a, b \in R\), \(x, y \in M\), we have
   1. \(a \bullet (x + y) = a \bullet x + b \bullet y\)
   2. \((a + b) \bullet x = a \bullet x + b \bullet x\)
   3. \(a * (b \bullet x)=(a * b) \bullet x\)
   4. \(1_R \bullet x = x\)

The notation of scalar multiplication is generalized as heterogeneous scalar multiplication HMul in \(\textsf {Mathlib}\): \[ \bullet : \alpha \to \beta \to \gamma \] where \(\alpha \), \(\beta \), \(\gamma \) are different types.

If \(R\) is a division ring, then a module \(M\) over \(R\) is called a vector space.

For generality, \(\textsf {Mathlib}\) uses Module throughout for vector spaces, particularly, for a vector space \(V\), it's usually declared as

For definitions/theorems about it, and most of them can be found under Mathlib.LinearAlgebra e.g. LinearIndependent.

A submodule \(N\) of \(M\) is a module \(N\) such that every element of \(N\) is also an element of \(M\). If \(M\) is a vector space then \(N\) is called a subspace.

The dual module \(M^* : M \to _{l[R]} R\) is the \(R\)-module of all linear maps from \(M\) to \(R\).