Mathlib Changelog
v4
Changelog
About
Github
Theorem
not_irrational_zero
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_zero
View on Github →