Theorem NNRat.den_ofNat

Modification history

2025-01-07 09:21

Mathlib/Data/NNRat/Defs.lean

chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) …

Modified NNRat.den_ofNat View on Github →

2024-05-05 18:04

Mathlib/Data/NNRat/Defs.lean

feat: more NNRat lemmas (#12586) …

Added NNRat.den_ofNat View on Github →