Theorem Nat.sqrt_succ_le_succ_sqrt

Modification history

2024-08-29 10:45
Mathlib/Data/Nat/Defs.lean
chore: split out Data.Nat.Sqrt (#16237)
Modified Nat.sqrt_succ_le_succ_sqrtView on Github →
2024-08-29 06:34
Mathlib/Data/Nat/Defs.lean
revert accidental pushes to master (#16242)
Modified Nat.sqrt_succ_le_succ_sqrtView on Github →
2024-08-29 14:40
Mathlib/Data/Nat/Sqrt.lean
chore: split out Data.Nat.Sqrt
Added Nat.sqrt_succ_le_succ_sqrtView on Github →
2024-08-29 14:40
Mathlib/Data/Nat/Defs.lean
chore: split out Data.Nat.Sqrt
Deleted Nat.sqrt_succ_le_succ_sqrtView on Github →
2024-04-08 02:32
Mathlib/Data/Nat/Defs.lean
chore(Data/Nat/Defs): Integrate `Nat.sqrt` material (#11866) …
Modified Nat.sqrt_succ_le_succ_sqrtView on Github →
2022-12-22 13:30
Mathlib/Data/Nat/Sqrt.lean
feat: Port `Data.Nat.Sqrt` (#1142) …
Added Nat.sqrt_succ_le_succ_sqrtView on Github →