mathlib

151f0dd2 - chore(linear_algebra/tensor_product): missing simp lemmas (#4769)