Commit 2024-02-03 14:26 3752900e

View on Github →

refactor: Make Nat.floorRoot computable (#10208) Avoiding Finsupp.mapRange means that we can actually compute the function.

Estimated changes

Modified Mathlib/Algebra/Order/Floor/Div.lean

modified theorem Finsupp.ceilDiv_def

added theorem Finsupp.coe_ceilDiv_def

added theorem Finsupp.coe_floorDiv

modified theorem Finsupp.floorDiv_def

Modified Mathlib/Data/Nat/Factorization/Root.lean

added def Nat.ceilRoot

added theorem Nat.ceilRoot_def

added def Nat.floorRoot

added theorem Nat.floorRoot_def