# mathlibdocumentation

ring_theory.free_ring

# Free rings

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 f.
• map (f : α → β) : the ring hom free_ring α →+* free_ring β induced by f.

## Implementation details

free_ring α is implemented as the free abelian group over the free monoid on α.

## Tags

free ring

def free_ring  :
Type uType u

The free ring over a type α.

Equations
@[instance]
def free_ring.ring (α : Type u) :

Equations
@[instance]
def free_ring.inhabited (α : Type u) :

Equations
def free_ring.of {α : Type u} :
α →

The canonical map from α to free_ring α.

Equations
theorem free_ring.induction_on {α : Type u} {C : → Prop} (z : free_ring α) :
C (-1)(∀ (b : α), C (free_ring.of b))(∀ (x y : , C xC yC (x + y))(∀ (x y : , C xC yC (x * y))C z

def free_ring.lift {α : Type u} {R : Type v} [ring R] :
(α → R) →+* R

The ring homomorphism free_ring α →+* R induced from a map α → R.

Equations
@[simp]
theorem free_ring.lift_of {α : Type u} {R : Type v} [ring R] (f : α → R) (x : α) :

@[simp]
theorem free_ring.lift_comp_of {α : Type u} {R : Type v} [ring R] (f : →+* R) :

def free_ring.map {α : Type u} {β : Type v} :
(α → β)

The canonical ring homomorphism free_ring α →+* free_ring β generated by a map α → β.

Equations
@[simp]
theorem free_ring.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :