Commit 2024-06-18 08:57 72ae24be

feat: Irrational √q iff ¬IsSquare q for Nat/Int/Rat (#13867) This enables proofs like

unseal Nat.sqrt.iter in
example : Irrational √24 := by decide

This also deprecates the old irrational_sqrt_rat_iff in favor of the new irrational_sqrt_ratCast_iff, which is better-named and -stated. Zulip motivation.

Estimated changes

Modified Mathlib/Data/Real/Irrational.lean

added theorem Irrational.ne_ofNat

added theorem irrational_sqrt_intCast_iff

added theorem irrational_sqrt_intCast_iff_of_nonneg

added theorem irrational_sqrt_natCast_iff

added theorem irrational_sqrt_ofNat_iff

added theorem irrational_sqrt_ratCast_iff

added theorem irrational_sqrt_ratCast_iff_of_nonneg

added theorem not_irrational_ofNat

added theorem not_irrational_one

added theorem not_irrational_zero