Commit 2024-08-29 14:40 89c51aac

View on Github →

chore: split out Data.Nat.Sqrt

Estimated changes

Modified Mathlib/Algebra/Group/Nat.lean

Modified Mathlib/Data/Int/Sqrt.lean

Modified Mathlib/Data/Nat/Defs.lean

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

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

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

deleted theorem Nat.sqrt_one

deleted theorem Nat.sqrt_pos

deleted theorem Nat.sqrt_succ_le_succ_sqrt

deleted theorem Nat.sqrt_zero

deleted theorem Nat.succ_le_succ_sqrt'

deleted theorem Nat.succ_le_succ_sqrt

Modified Mathlib/Data/Nat/Pairing.lean