Commit 2024-06-15 21:43 48de726c

View on Github →

feat: norm_cast lemmas about IsSquare and {Int,Rat}.sqrt (#13788)

Estimated changes

Modified Mathlib/Algebra/Ring/Int.lean

added theorem Int.isSquare_natCast_iff

added theorem Int.isSquare_ofNat_iff

Modified Mathlib/Data/Int/Sqrt.lean

added theorem Int.sqrt_natCast

added theorem Int.sqrt_ofNat

Modified Mathlib/Data/Rat/Lemmas.lean

added theorem Rat.isSquare_iff

added theorem Rat.isSquare_intCast_iff

added theorem Rat.isSquare_natCast_iff

added theorem Rat.isSquare_ofNat_iff

Modified Mathlib/Data/Rat/Sqrt.lean

added theorem Rat.sqrt_intCast

added theorem Rat.sqrt_natCast

added theorem Rat.sqrt_ofNat