Commit 2020-09-29 12:11 744e0675

View on Github →

feat(linear_algebra/dual): transpose of linear maps (#4302) This is filling an easy hole from the undergrad curriculum page: the transpose of a linear map. We don't prove much about it but at least we make contact with matrix transpose.

Estimated changes

Modified docs/undergrad.yaml

Modified src/linear_algebra/basic.lean

added theorem linear_equiv.arrow_congr_symm_apply

Modified src/linear_algebra/dual.lean

added theorem is_basis.dual_basis_apply

added theorem is_basis.dual_basis_apply_self

added theorem is_basis.dual_basis_equiv_fun

added theorem is_basis.dual_basis_repr

added theorem is_basis.to_dual_apply_left

added theorem is_basis.to_dual_apply_right

added theorem is_basis.to_dual_eq_equiv_fun

added theorem is_basis.to_dual_total_left

added theorem is_basis.to_dual_total_right

added theorem is_basis.total_dual_basis

added def module.dual.transpose

added theorem module.dual.transpose_apply

added theorem module.dual.transpose_comp

Modified src/linear_algebra/matrix.lean

added theorem linear_equiv_matrix'_symm_apply

added theorem linear_equiv_matrix_symm_apply

added theorem linear_equiv_matrix_symm_transpose

added theorem linear_equiv_matrix_transpose