Commit 2021-02-22 14:12 12bb9aee

View on Github →

chore(linear_algebra/*): split lines and doc direct_sum/tensor_product (#6360) This PR provides a short module doc to direct_sum/tensor_product (the file contains only one result). Furthermore, it splits lines in the linear_algebra folder.

Estimated changes

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/char_poly/coeff.lean

modified theorem finite_field.trace_pow_card

Modified src/linear_algebra/determinant.lean

Modified src/linear_algebra/direct_sum/finsupp.lean

Modified src/linear_algebra/direct_sum/tensor_product.lean

Modified src/linear_algebra/matrix.lean

modified theorem linear_map.trace_eq_matrix_trace

Modified src/linear_algebra/special_linear_group.lean