Commit 2024-08-29 14:40 f0887abf

View on Github →

chore: split out Data.Nat.Sqrt

Estimated changes

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.iter_sq_le

added theorem Nat.sqrt.lt_iter_succ_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