Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-20 17:09 b0805a5e

View on Github →

feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace (#10372)

Estimated changes

Modified src/data/finsupp/basic.lean

added theorem finsupp.single_smul

added theorem finsupp.sum_univ_single'

added theorem finsupp.sum_univ_single

Modified src/data/matrix/basis.lean

added theorem matrix.std_basis_matrix.diag_same

Modified src/linear_algebra/contraction.lean

added theorem dual_tensor_hom_equiv_of_basis_to_linear_map

added theorem to_matrix_dual_tensor_hom

Modified src/linear_algebra/dual.lean

added theorem basis.sum_dual_apply_smul_coord

Modified src/linear_algebra/tensor_product_basis.lean

added theorem basis.tensor_product_apply'

added theorem basis.tensor_product_apply

Modified src/linear_algebra/trace.lean

added theorem linear_map.trace_eq_contract'

added theorem linear_map.trace_eq_contract

added theorem linear_map.trace_eq_contract_of_basis'

added theorem linear_map.trace_eq_contract_of_basis

Modified src/representation_theory/basic.lean

modified theorem representation.char_one