Commit 2020-07-21 07:47 d174d3d0

View on Github →

refactor(linear_algebra/*): postpone importing material on direct sums (#3484) This is just a refactor, to avoid needing to develop material on direct sums before we can even define an algebra.

Estimated changes

Modified src/algebra/direct_limit.lean

Modified src/algebra/lie_algebra.lean

Created src/linear_algebra/direct_sum/finsupp.lean

added def finsupp_lequiv_direct_sum

added theorem finsupp_lequiv_direct_sum_single

added theorem finsupp_lequiv_direct_sum_symm_lof

added def finsupp_tensor_finsupp

added theorem finsupp_tensor_finsupp_single

added theorem finsupp_tensor_finsupp_symm_single

Created src/linear_algebra/direct_sum/tensor_product.lean

added def tensor_product.direct_sum

added theorem tensor_product.direct_sum_lof_tmul_lof

Modified src/linear_algebra/finsupp.lean

deleted def finsupp_lequiv_direct_sum

deleted theorem finsupp_lequiv_direct_sum_single

deleted theorem finsupp_lequiv_direct_sum_symm_lof

deleted def finsupp_tensor_finsupp

deleted theorem finsupp_tensor_finsupp_single

deleted theorem finsupp_tensor_finsupp_symm_single

Modified src/linear_algebra/finsupp_vector_space.lean

Modified src/linear_algebra/tensor_product.lean

deleted def tensor_product.direct_sum

deleted theorem tensor_product.direct_sum_lof_tmul_lof