feat(Algebra/DirectSum): equivalence between direct sum indexed by ι₁ and double sum indexed by ι₂ and fibres of f : ι₁ → ι₂#39607
Open
TentativeConvert wants to merge 30 commits into
Commits
Commits on May 19, 2026
Commits on May 20, 2026
Commits on Jun 22, 2026
- andauthored
Commits on Jun 23, 2026
- committed
- committed
- committed
- andauthored
- andauthored
- committed
- andauthored
- andauthored
- andauthored
- andauthored
- committed
- committed
Commits on Jun 24, 2026
- andauthored
- committed
- committed
- committed
- committed
Commits on Jun 27, 2026
- andauthored
- committed