chore(LinearAlgebra/DirectSum/TensorProduct): missing lemma

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4

https://leanprover-community.github.io/lean3

Apache License 2.0

1.67k stars 298 forks source link

Closed eric-wieser closed 1 year ago

eric-wieser commented 1 year ago

We had the lemma about how the forward direction of this equivalence behaves, but not the reverse direction.