Commit 2025-01-18 22:00 bdee03dd

View on Github →

chore(Dynamics/PeriodicPts): don't import MonoidWithZero (#20765) For this, split the file into .Defs and .Lemmas.

Estimated changes