Commit 2023-04-07 15:02 861c8732

View on Github →

feat: port LinearAlgebra.Multilinear.TensorProduct (#3328)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean

added def MultilinearMap.domCoprod'

added theorem MultilinearMap.domCoprod'_apply

added def MultilinearMap.domCoprod

added theorem MultilinearMap.domCoprod_domDomCongr_sumCongr