The theory of the free ring over a type.
free_ring α: the free (not commutative in general) ring over a type.
lift (f : α → R): the ring hom
free_ring α →+* Rinduced by
map (f : α → β): the ring hom
free_ring α →+* free_ring βinduced by
free_ring α is implemented as the free abelian group over the free monoid on
The ring homomorphism
free_ring α →+* R induced from a map
α → R.