Theorem Rat.isNat_intFloor_ofIsNNRat

Modification history

2025-08-13 09:12
Mathlib/Data/Rat/Floor.lean
refactor: Add norm_num machinery for NNRat (#9915) …
Added Rat.isNat_intFloor_ofIsNNRatView on Github →