## Stream: maths

### Topic: odd numbers

#### Patrick Massot (Oct 05 2020 at 19:05):

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 (Oct 05 2020 at 20:13):

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 (Oct 05 2020 at 20:24):

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 (Oct 05 2020 at 21:30):

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 (Oct 05 2020 at 22:31):

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

#### Ruben Van de Velde (Oct 06 2020 at 08:13):

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

#### Patrick Massot (Oct 06 2020 at 08:30):

I'll open a PR soon

#### Patrick Massot (Oct 06 2020 at 09:07):

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

#### Patrick Massot (Oct 06 2020 at 09:25):

#4473

Last updated: May 14 2021 at 19:21 UTC