Mathlib Changelog
v4
Changelog
About
Github
Theorem
irrational_sqrt_ofNat_iff
Modification history
2024-06-18 08:57
Mathlib/Data/Real/Irrational.lean
feat: `Irrational √q` iff `¬IsSquare q` for `Nat`/`Int`/`Rat` (#13867) …
Added
irrational_sqrt_ofNat_iff
View on Github →