Theorem not_irrational_ofNat

Modification history

2025-01-02 08:45
Mathlib/Data/Real/Irrational.lean
chore: use `ofNat()` around `Real` and `Complex` (#20388) …
Modified not_irrational_ofNatView on Github →
2024-06-18 08:57
Mathlib/Data/Real/Irrational.lean
feat: `Irrational √q` iff `¬IsSquare q` for `Nat`/`Int`/`Rat` (#13867) …
Added not_irrational_ofNatView on Github →