Commit 2023-04-07 11:23 934f05d4

View on Github →

feat: port LinearAlgebra.TensorProductBasis (#3295)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/TensorProductBasis.lean

added def Basis.tensorProduct

added theorem Basis.tensorProduct_apply'

added theorem Basis.tensorProduct_apply