Free rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The theory of the free ring over a type.
Main definitions #
free_ring α : the free (not commutative in general) ring over a type.
lift (f : α → R) : the ring hom
free_ring α →+* R induced by
map (f : α → β) : the ring hom
free_ring α →+* free_ring β induced by
Implementation details #
free_ring α is implemented as the free abelian group over the free monoid on
The free ring over a type
The canonical map from α to
The ring homomorphism
free_ring α →+* R induced from a map
α → R.
The canonical ring homomorphism
free_ring α →+* free_ring β generated by a map
α → β.