Commit 2024-06-09 08:12 415fd9d7

View on Github →

chore: Add floor_ofNat and ceil_ofNat (#13645) Also renames Nat.floor_coe to floor_natCast, leaving behind a deprecation.

Estimated changes

added theorem Nat.ceil_ofNat
deleted theorem Nat.floor_coe
added theorem Nat.floor_natCast
added theorem Nat.floor_ofNat
modified theorem Nat.floor_one
modified theorem Nat.floor_zero