Commit 2023-05-22 19:47 9e514c71

View on Github →

feat: port LinearAlgebra.BilinearForm.TensorProduct (#4233)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

added def BilinForm.tensorDistrib

added theorem BilinForm.tensorDistribEquiv_apply

added theorem BilinForm.tensorDistrib_tmul