Commit 2024-04-08 02:32 d4b9a267

View on Github →

chore(Data/Nat/Defs): Integrate Nat.sqrt material (#11866) Move the content of Data.Nat.ForSqrt and Data.Nat.Sqrt to Data.Nat.Defs by using Nat-specific Std lemmas rather than the mathlib general ones. This makes it ready to move to Std if wanted.

Estimated changes

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.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_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_one
added theorem Nat.sqrt_pos
added theorem Nat.sqrt_zero
added theorem Nat.succ_le_succ_sqrt'
added theorem Nat.succ_le_succ_sqrt
deleted theorem Nat.sqrt.iter_sq_le
deleted theorem Nat.sqrt.lt_iter_succ_sq
modified theorem Nat.add_le_pair
deleted theorem Nat.eq_sqrt'
deleted theorem Nat.eq_sqrt
deleted theorem Nat.exists_mul_self'
deleted theorem Nat.exists_mul_self
deleted theorem Nat.le_sqrt'
deleted theorem Nat.le_sqrt
deleted theorem Nat.lt_succ_sqrt'
deleted theorem Nat.lt_succ_sqrt
deleted theorem Nat.not_exists_sq'
deleted theorem Nat.not_exists_sq
deleted theorem Nat.sqrt_add_eq'
deleted theorem Nat.sqrt_add_eq
deleted theorem Nat.sqrt_eq'
deleted theorem Nat.sqrt_eq
deleted theorem Nat.sqrt_eq_zero
deleted theorem Nat.sqrt_le'
deleted theorem Nat.sqrt_le
deleted theorem Nat.sqrt_le_add
deleted theorem Nat.sqrt_le_self
deleted theorem Nat.sqrt_le_sqrt
deleted theorem Nat.sqrt_lt'
deleted theorem Nat.sqrt_lt
deleted theorem Nat.sqrt_lt_self
deleted theorem Nat.sqrt_mul_sqrt_lt_succ
deleted theorem Nat.sqrt_one
deleted theorem Nat.sqrt_pos
deleted theorem Nat.sqrt_zero
deleted theorem Nat.succ_le_succ_sqrt'
deleted theorem Nat.succ_le_succ_sqrt