Theorem Rat.num_inv

Modification history

2025-09-15 12:54
Mathlib/Data/Rat/Lemmas.lean
chore: bump toolchain to v4.24.0-rc1 (#29671)
Deleted Rat.num_invView on Github →
2025-06-25 13:48
Mathlib/Data/Rat/Lemmas.lean
feat: `(q⁻¹).num` and `(q⁻¹).den` for `q : ℚ` (#26381) …
Added Rat.num_invView on Github →