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.