Commit 2022-03-29 09:36 89c8112f
View on Github →feat(topology/algebra/monoid): finprod is eventually equal to finset.prod (#13013)
Motivated by https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Using.20partitions.20of.20unity
feat(topology/algebra/monoid): finprod is eventually equal to finset.prod (#13013)
Motivated by https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Using.20partitions.20of.20unity