odd numbers

Stream: maths

[Patrick Massot]

I missed #4357 that introduced odd numbers in mathlib until it broke the tutorials project automatic update. Of course I'm extremely grateful that someone defined int.odd, not having it was extremely weird. However I don't understand why this definition was chosen. Why not def int.odd (n : ℤ) := ∃ k, n = 2*k + 1? We could even have it for a general semiring. This makes it completely analogous to even, and allow to use rintro/rcases directly on an assumption odd n. Also, shouldn't we put pp_nodot on even and odd?

[Joseph Myers]

My assumption was that it was deliberate that even was defined without odd, so given that odd was wanted to allow more literal formal expression of informal statements that say "odd", it should be defined as simply as possible in terms of even and simp should convert it to be in terms of even. If it turns out a different definition (or different handling in simp) is useful, including a definition for general semirings, that's fine with me.

[Kyle Miller]

What's an example of this other definition of odd being useful for semirings? (And, having no theorem in mind, why not generalize it more? "An element $x$ is odd if there is a unit $u$ and another element $y$ such that $x=2y+u$.")

[Patrick Massot]

I really meant I'd like to have the nice definition for integers and natural numbers. I don't care about other semi-rings here.

[Yury G. Kudryashov]

We can have any definition (e.g., not even) and add ∃ k, 2 * k + 1 = n as odd.exists.

[Ruben Van de Velde]

I've got that proof lying around, if people want it

[Patrick Massot]

I'll open a PR soon

[Ruben Van de Velde]

@Patrick Massot fyi https://gist.github.com/Ruben-VandeVelde/bfc190d3334b6f423015012ffd4e2b77

[Patrick Massot]

Thanks Ruben, but I think we already have everything that is needed here.

[Patrick Massot]

#4473