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
.
chore(Dynamics/PeriodicPts): don't import MonoidWithZero
(#20765)
For this, split the file into .Defs
and .Lemmas
.