Commit 2023-03-20 10:43 fc708bb9

View on Github →

feat: port Algebra/FreeAlgebra (#2905)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/FreeAlgebra.lean

added def FreeAlgebra.Pre.hasAdd

added def FreeAlgebra.Pre.hasCoeGenerator

added def FreeAlgebra.Pre.hasCoeSemiring

added def FreeAlgebra.Pre.hasMul

added def FreeAlgebra.Pre.hasOne

added def FreeAlgebra.Pre.hasSmul

added def FreeAlgebra.Pre.hasZero

added inductive FreeAlgebra.Pre

added inductive FreeAlgebra.Rel

added theorem FreeAlgebra.algebraMap_eq_one_iff

added theorem FreeAlgebra.algebraMap_eq_zero_iff

added theorem FreeAlgebra.algebraMap_inj

added theorem FreeAlgebra.algebraMap_leftInverse

added theorem FreeAlgebra.hom_ext

added theorem FreeAlgebra.induction

added theorem FreeAlgebra.liftAux_eq

added theorem FreeAlgebra.lift_comp_ι

added theorem FreeAlgebra.lift_symm_apply

added theorem FreeAlgebra.lift_unique

added theorem FreeAlgebra.lift_ι_apply

added theorem FreeAlgebra.quot_mk_eq_ι

added theorem FreeAlgebra.ι_comp_lift

added theorem FreeAlgebra.ι_inj

added theorem FreeAlgebra.ι_injective

added theorem FreeAlgebra.ι_ne_algebraMap

added theorem FreeAlgebra.ι_ne_one

added theorem FreeAlgebra.ι_ne_zero

added def FreeAlgebra