Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-30 20:39 e70093ff

View on Github →

feat(algebra/free_non_unital_non_assoc_algebra): construction of the free non-unital, non-associative algebra on a type X with coefficients in a semiring R (#8141)

Estimated changes

Modified src/algebra/free_algebra.lean

Created src/algebra/free_non_unital_non_assoc_algebra.lean

added theorem free_non_unital_non_assoc_algebra.hom_ext

added def free_non_unital_non_assoc_algebra.lift

added theorem free_non_unital_non_assoc_algebra.lift_comp_of

added theorem free_non_unital_non_assoc_algebra.lift_of_apply

added theorem free_non_unital_non_assoc_algebra.lift_symm_apply

added theorem free_non_unital_non_assoc_algebra.lift_unique

added def free_non_unital_non_assoc_algebra.of

added theorem free_non_unital_non_assoc_algebra.of_comp_lift

added def free_non_unital_non_assoc_algebra