mathlib

c4f91767 - feat(linear_algebra/tensor_product): ite_tmul (#3216)

feat(linear_algebra/tensor_product): ite_tmul (#3216) ``` ((if P then x₁ else 0) ⊗ₜ[R] x₂) = if P then (x₁ ⊗ₜ x₂) else 0 ``` and the symmetric version. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>