a^2 is even -> a is even

Stream: new members

[ROCKY KAMEN-RUBIO]

I vaguely remember seeing a proof of this in a tutorial somewhere that didn't use anything about nats being even or odd. Does anyone remember where this could have been, or if I'm remembering this correctly? Thanks!

[Jason KY.]

Is this what you are looking for?
https://github.com/leanprover-community/tutorials/blob/master/src/solutions/07_first_negations.lean#L153

[Kevin Buzzard]

It's in the lean tutorial but there you are told explicitly to use that something is odd if it's not even. You can prove it using uniqueness of prime factorisation but in some sense this is circular, division with remainder is needed to prove that

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

It's in the lean tutorial but there you are told explicitly to use that something is odd if it's not even. You can prove it using uniqueness of prime factorisation but in some sense this is circular, division with remainder is needed to prove that

That makes sense now why I wasn't able to reproduce it on my own lol. Thanks!