Theorem Int.sqrt_natCast

Modification history

2025-04-27 19:30

Mathlib/Data/Int/Sqrt.lean

chore: prepare for the next lean version bump (#24417) …

Modified Int.sqrt_natCast View on Github →

2024-06-15 21:43

Mathlib/Data/Int/Sqrt.lean

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

Added Int.sqrt_natCast View on Github →