Timeline for Need help with induction proof in Lean for $0+d=d$
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 22 at 14:21 | vote | accept | CrSb0001 | ||
| Jan 20 at 2:27 | history | edited | CrSb0001 |
added lean4 tag since it is needed here
|
|
| Jan 19 at 17:21 | answer | added | CrSb0001 | timeline score: 1 | |
| Jan 19 at 16:23 | comment | added | Kevin Buzzard | Just use induction once :-) | |
| Jan 19 at 16:01 | comment | added | Ricky | Ah, I see, you are trying to prove even the induction step by induction. Well, this is not a very good idea. But notice that you now have a new assumption! | |
| Jan 19 at 15:54 | comment | added | Ricky |
Can you explain better the problem? If you want to prove 0+d=d by induction (that is a very good idea), the two cases should be 0+0=0 and 0 + succ d = succ d knowing that 0 + d = d.
|
|
| S Jan 19 at 15:46 | review | First questions | |||
| Jan 20 at 1:07 | |||||
| S Jan 19 at 15:46 | history | asked | CrSb0001 | CC BY-SA 4.0 |