Commit 2024-02-28 08:33 f5e8fa18

View on Github →

feat(LinearAlgebra/TensorProduct): add TensorProduct.map₂ (#10986)

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct.lean

added def TensorProduct.map₂

added theorem TensorProduct.map₂_apply_tmul

Modified Mathlib/RingTheory/TensorProduct.lean

deleted def Algebra.TensorProduct.mulAux

deleted theorem Algebra.TensorProduct.mulAux_apply