Multiplying by 2

Stream: new members

[Emiel Lanckriet]

I'm making a Odd + Even = Odd? Even * Anything = Even? Prove it!-kata on Codewars, but I'm stuck even_mul_even, I know that n is even and I know that sums of even numbers are even, now I want to show that that n * 2 is even, but I can't find a way to convert n * 2 to n + n. Any advice?

[Kevin Buzzard]

I guess you could prove it by induction

[Kevin Buzzard]

When I did that kata I proved a couple of things which weren't asked for, to make my life easier.

[Emiel Lanckriet]

Ok, thanks I'll try to prove n*2=n+n by induction in a separate function.

[Kevin Buzzard]

I guess we're hoping to keep codewars spoiler questions off this site in general, although most Lean questions are welcomed :-)

[Mario Carneiro]

I'm not sure I like this, we've never had to censor solutions before, despite several lean classes being taught

[Mario Carneiro]

It means that the more people make katas the less we can talk about, and the censorship has no end date

[Mario Carneiro]

anyway, there is a theorem two_mul

[Emiel Lanckriet]

Is there a place where I can easily look up these theorems, because for the moment I look at the sidelines of the natural numbers game, but some of it doesn't translate to Lean in general.

[Mario Carneiro]

there is the lean docs

[Shing Tak Lam]

Are you using VSCode? if so, press Ctrl-P and then # if you know what the name should be (approximately).

[Mario Carneiro]

https://leanprover-community.github.io/mathlib_docs/

[Emiel Lanckriet]

Thanks, for now I am just using CoCalc.

[Mario Carneiro]

there is also grep on the sources

[Mario Carneiro]

or your favorite not-grep

[Mario Carneiro]

and library_search

[Donald Sebastian Leung]

IMO general hints and tips for solving Codewars kata is okay, but don't e.g. post your Codewars solutions publicly on GitHub (because then others could just copy and paste full solutions to get free points)

[Emiel Lanckriet]

I have been looking for the inverse of succ_inj in the docs, but I can't find it does someone know where to find this? In the natural number game it is called succ_eq_succ_of_eq, but in the mathlib_docs I can't find anything similar.

[Mario Carneiro]

congr_arg is a theorem that proves x = y -> f x = f y once and for all. The tactic is congr

[Emiel Lanckriet]

Wow, thanks, that's much more powerfull than what I needed.