Theorems · Definition · ring theory

FreeRing

Type u → Type u

If α is a type, then FreeRing α is the free ring generated by α. This is a ring equipped with a function FreeRing.of : α → FreeRing α which has the following universal property: if R is any ring, and f : α → R is any function, then this function is the composite of FreeRing.of and a unique ring homomorphism FreeRing.lift f : FreeRing α →+* R. A typical element of FreeRing α is a ℤ-linear combination of formal products of elements of α. For example if x and y are terms of type α then 3 * x * y * x - 2 * y * x + 1 is a "typical" element of FreeRing α. In particular if α is empty then FreeRing α is isomorphic to ℤ, and if α has one term t then FreeRing α is isomorphic to the polynomial ring ℤ[t]. If α has two or more terms then FreeRing α is not commutative. One can think of FreeRing α as the free non-commutative polynomial ring with coefficients in the integers and variables indexed by α.

Defined in

Mathlib.RingTheory.FreeRing

Cited by

20 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound