Commit 2022-12-22 13:30 336525b4

View on Github →

feat: Port Data.Nat.Sqrt (#1142) ba2245edf0c8bb155f1569fd9b9492a9b384cde6

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/ForSqrt.lean

added theorem Nat.sqrt.iter_sq_le

added theorem Nat.sqrt.lt_iter_succ_sq

Created Mathlib/Data/Nat/Sqrt.lean

added theorem Nat.eq_sqrt'

added theorem Nat.eq_sqrt

added theorem Nat.exists_mul_self'

added theorem Nat.exists_mul_self

added theorem Nat.le_sqrt'

added theorem Nat.le_sqrt

added theorem Nat.le_three_of_sqrt_eq_one

added theorem Nat.lt_succ_sqrt'

added theorem Nat.lt_succ_sqrt

added theorem Nat.not_exists_sq'

added theorem Nat.not_exists_sq

added theorem Nat.sqrt_add_eq'

added theorem Nat.sqrt_add_eq

added theorem Nat.sqrt_eq'

added theorem Nat.sqrt_eq

added theorem Nat.sqrt_eq_zero

added theorem Nat.sqrt_le'

added theorem Nat.sqrt_le

added theorem Nat.sqrt_le_add

added theorem Nat.sqrt_le_self

added theorem Nat.sqrt_le_sqrt

added theorem Nat.sqrt_lt'

added theorem Nat.sqrt_lt

added theorem Nat.sqrt_lt_self

added theorem Nat.sqrt_mul_sqrt_lt_succ'

added theorem Nat.sqrt_mul_sqrt_lt_succ

added theorem Nat.sqrt_one

added theorem Nat.sqrt_pos

added theorem Nat.sqrt_succ_le_succ_sqrt

added theorem Nat.sqrt_zero

added theorem Nat.succ_le_succ_sqrt'

added theorem Nat.succ_le_succ_sqrt