Theorem Rat.isSquare_ofNat_iff

Modification history

2024-06-15 21:43

Mathlib/Data/Rat/Lemmas.lean

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

Added Rat.isSquare_ofNat_iff View on Github →