mathlib3

chore(LinearAlgebra/DirectSum/TensorProduct): missing lemma

#19242

Closed