Commit 2024-08-29 06:34 8cebd9ee

View on Github →

revert accidental pushes to master (#16242)

Estimated changes

Modified Mathlib/Algebra/Group/Nat.lean

Modified Mathlib/Data/Int/Sqrt.lean

Modified Mathlib/Data/Nat/Defs.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

Modified Mathlib/Data/Nat/Pairing.lean

Deleted Mathlib/Data/Nat/Sqrt.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