Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-17 15:33 34ebade1

View on Github →

feat(algebra/free_algebra): free (noncommutative) algebras (#4077) Previously, @adamtopaz constructed the tensor algebra of an R-module via a direct construction of a quotient of a free algebra. This uses essentially the same construction to build a free algebra (on a type) directly. In a PR coming shortly, I'll refactor his development of the tensor algebra to use this construction.

Estimated changes

Created src/algebra/free_algebra.lean

added def free_algebra.equiv_monoid_algebra_free_monoid

added theorem free_algebra.hom_ext

added def free_algebra.lift

added theorem free_algebra.lift_comp_ι

added def free_algebra.lift_fun

added theorem free_algebra.lift_unique

added theorem free_algebra.lift_ι_apply

added def free_algebra.pre.has_add

added def free_algebra.pre.has_coe_generator

added def free_algebra.pre.has_coe_semiring

added def free_algebra.pre.has_mul

added def free_algebra.pre.has_one

added def free_algebra.pre.has_scalar

added def free_algebra.pre.has_zero

added inductive free_algebra.pre

added theorem free_algebra.quot_mk_eq_ι

added inductive free_algebra.rel

added def free_algebra.ι

added theorem free_algebra.ι_comp_lift

added def free_algebra

Modified src/data/monoid_algebra.lean

Modified src/linear_algebra/tensor_algebra.lean