Zulip Chat Archive

Stream: maths

Topic: odd numbers


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 xx is odd if there is a unit uu and another element yy such that x=2y+ux=2y+u.")

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ruben Van de Velde (Oct 06 2020 at 08:13):

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

view this post on Zulip Patrick Massot (Oct 06 2020 at 08:30):

I'll open a PR soon

view this post on Zulip Ruben Van de Velde (Oct 06 2020 at 09:05):

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

view this post on Zulip Patrick Massot (Oct 06 2020 at 09:07):

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

view this post on Zulip Patrick Massot (Oct 06 2020 at 09:25):

#4473


Last updated: May 14 2021 at 19:21 UTC