mathlib3 documentation


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 #

Implementation details #

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

Tags #

free ring

def free_ring (α : Type u) :

The free ring over a type α.

Instances for free_ring
@[protected, instance]
@[protected, instance]
def free_ring.ring (α : Type u) :
def free_ring.of {α : Type u} (x : α) :

The canonical map from α to free_ring α.

theorem free_ring.induction_on {α : Type u} {C : free_ring α Prop} (z : free_ring α) (hn1 : C (-1)) (hb : (b : α), C (free_ring.of b)) (ha : (x y : free_ring α), C x C y C (x + y)) (hm : (x y : free_ring α), C x C y C (x * y)) :
C z
def free_ring.lift {α : Type u} {R : Type v} [ring R] :
R) (free_ring α →+* R)

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

theorem free_ring.lift_of {α : Type u} {R : Type v} [ring R] (f : α R) (x : α) :
theorem free_ring.lift_comp_of {α : Type u} {R : Type v} [ring R] (f : free_ring α →+* R) :
theorem free_ring.hom_ext {α : Type u} {R : Type v} [ring R] ⦃f g : free_ring α →+* R⦄ (h : (x : α), f (free_ring.of x) = g (free_ring.of x)) :
f = g
def {α : Type u} {β : Type v} (f : α β) :

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

theorem free_ring.map_of {α : Type u} {β : Type v} (f : α β) (x : α) :