Theorem Rat.den_inv_of_ne_zero

Modification history

2025-06-25 13:48
Mathlib/Data/Rat/Lemmas.lean
feat: `(q⁻¹).num` and `(q⁻¹).den` for `q : ℚ` (#26381) …
Added Rat.den_inv_of_ne_zeroView on Github →