Free rings #
The theory of the free ring over a type.
Main definitions #
FreeRing α
: the free (not commutative in general) ring over a type.lift (f : α → R)
: the ring homFreeRing α →+* R
induced byf
.map (f : α → β)
: the ring homFreeRing α →+* FreeRing β
induced byf
.
Implementation details #
FreeRing α
is implemented as the free abelian group over the free monoid on α
.
Tags #
free ring
The free ring over a type α
.
Instances For
The canonical map from α to FreeRing α
.
Instances For
The ring homomorphism FreeRing α →+* R
induced from a map α → R
.
Instances For
@[simp]
@[simp]
@[simp]