Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-20 00:00 9232032b

View on Github →

refactor(linear_algebra/tensor_algebra): build as a quotient of a free algebra (#4079)

Estimated changes

Modified src/linear_algebra/tensor_algebra.lean

modified theorem tensor_algebra.hom_ext

deleted def tensor_algebra.lift_fun

added theorem tensor_algebra.lift_ι_apply

deleted def tensor_algebra.pre.has_add

deleted def tensor_algebra.pre.has_coe_module

deleted def tensor_algebra.pre.has_coe_semiring

deleted def tensor_algebra.pre.has_mul

deleted def tensor_algebra.pre.has_one

deleted def tensor_algebra.pre.has_scalar

deleted def tensor_algebra.pre.has_zero

deleted inductive tensor_algebra.pre

modified inductive tensor_algebra.rel

added theorem tensor_algebra.ring_quot_mk_alg_hom_free_algebra_ι_eq_ι

modified def tensor_algebra