Timeline for How to write a proof of n + 0 = n in Lean 4 using the built in definition of addition for Nats and not the theorem for Nat.add_zero?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 1 at 3:24 | comment | added | Jason Rute | Just to be pedantic the definition of addition on Nat doesn’t live in mathlib. It is in core Lean. The only part of your question requiring mathlib is the notation ℕ. | |
| S May 31 at 23:35 | history | suggested | hardmath | CC BY-SA 4.0 |
fix typo in title
|
| May 29 at 18:01 | review | Suggested edits | |||
| S May 31 at 23:35 | |||||
| May 29 at 0:23 | answer | added | Jason Rute | timeline score: 2 | |
| May 28 at 1:23 | answer | added | Chris Bailey | timeline score: 2 | |
| May 27 at 23:58 | history | asked | Charlie Parker | CC BY-SA 4.0 |