Commit 2024-09-29 06:55 ae458abd
View on Github →chore: robustify usage of List.prod API (#17220) Remove some reliances on defeq, and use some named arguments. I'm hoping to subsequently change the defeq, in https://github.com/leanprover-community/mathlib4/pull/17223