Theorem Nat.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.succ_le_succ_sqrtView on Github →2024-08-29 06:34
Mathlib/Data/Nat/Defs.lean
revert accidental pushes to master (#16242)
Modified Nat.succ_le_succ_sqrtView on Github →2024-08-29 14:40
Mathlib/Data/Nat/Sqrt.lean
chore: split out Data.Nat.Sqrt
Added Nat.succ_le_succ_sqrtView on Github →2024-08-29 14:40
Mathlib/Data/Nat/Defs.lean
chore: split out Data.Nat.Sqrt
Deleted Nat.succ_le_succ_sqrtView on Github →