Commit 2023-04-06 22:39 a897757a

View on Github →

chore: Generalise instances (#3304) Match https://github.com/leanprover-community/mathlib/pull/15171

Estimated changes

modified theorem TopologicalGroup.t2Space
modified theorem TopologicalGroup.t3Space
modified theorem tsum_comm
modified theorem tsum_prod
modified theorem tsum_sigma