Theorem Nat.sqrt_one
Modification history
2025-07-01 15:20
Mathlib/Data/Nat/Sqrt.lean
feat: use grind in Data/Nat/Sqrt (#26575) …
Modified Nat.sqrt_oneView on Github →2024-08-29 10:45
Mathlib/Data/Nat/Defs.lean
chore: split out Data.Nat.Sqrt (#16237)
Modified Nat.sqrt_oneView on Github →2024-08-29 06:34
Mathlib/Data/Nat/Defs.lean
revert accidental pushes to master (#16242)
Modified Nat.sqrt_oneView on Github →2024-08-29 14:40
Mathlib/Data/Nat/Sqrt.lean
chore: split out Data.Nat.Sqrt
Added Nat.sqrt_oneView on Github →2024-08-29 14:40
Mathlib/Data/Nat/Defs.lean
chore: split out Data.Nat.Sqrt
Deleted Nat.sqrt_oneView on Github →