Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-08 17:19 7c67c296

View on Github →

feat(data/nat/sqrt): ported data/nat/sqrt.lean from Lean2

Estimated changes

Created data/nat/sqrt.lean

added theorem nat.eq_zero_of_sqrt_eq_zero

added theorem nat.le_three_of_sqrt_eq_one

added theorem nat.mul_square_cancel

added theorem nat.sqrt_eq

added theorem nat.sqrt_lower

added theorem nat.sqrt_lt

added theorem nat.sqrt_mono

added theorem nat.sqrt_mul_eq

added theorem nat.sqrt_pos_of_pos

added theorem nat.sqrt_upper