Commit 2024-06-18 08:57 72ae24be

View on Github →

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