feat(Algebra/DirectSum): equivalence between direct sum indexed by ι₁ and double sum indexed by ι₂ and fibres of f : ι₁ → ι₂#39607

TentativeConvert wants to merge 30 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

TentativeConvert:sigma-fiber-equivTentativeConvert/mathlib4:sigma-fiber-equivCopy head branch name to clipboard