Theorem irrational_sqrt_ratCast_iff_of_nonneg

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_ratCast_iff_of_nonnegView on Github →