Theorem not_irrational_one

Modification history

2024-06-18 08:57
Mathlib/Data/Real/Irrational.lean
feat: `Irrational √q` iff `¬IsSquare q` for `Nat`/`Int`/`Rat` (#13867) …
Added not_irrational_oneView on Github →