search

leanprover-community / mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.66k stars 297 forks source link

chore(LinearAlgebra/DirectSum/TensorProduct): missing lemma #19242

Closed eric-wieser closed 9 months ago

eric-wieser commented 9 months ago

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

Open in Gitpod