Commit 2020-10-19 07:13 41c227a1
View on Github →feat(algebra/infinite_sum): make tsum irreducible (#4679) See https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/congr'.20is.20slow
feat(algebra/infinite_sum): make tsum irreducible (#4679) See https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/congr'.20is.20slow