Theorem Int.sqrt_ofNat

Modification history

2025-01-01 21:42

Mathlib/Data/Int/Sqrt.lean

refactor: add an ofNat() elaborator (#20169) …

Modified Int.sqrt_ofNat 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_ofNat View on Github →