Commit 2023-06-24 05:35 2daf260f

View on Github →

chore: don't use simps (#5423) simps unfolds too much and it produces useless declarations. These are those present in mathlib3.

Estimated changes