data.nat.parity

Stream: Is there code for X?

[Patrick Johnson]

I very often use these theorems:

lemma add_div_eq_succ_div {n m : ℕ} (h : 0 < m) : (n + m) / m = n / m + 1
lemma pos_of_odd {n : ℕ} (h : odd n) : 0 < n
lemma even_div_2 {n : ℕ} (h : even n) : n / 2 * 2 = n
lemma odd_div_2 {n : ℕ} (h : odd n) : n / 2 * 2 + 1 = n
lemma odd_div_2' {n : ℕ} (h : odd n) : n / 2 * 2 = n - 1

All of them are easy to prove, but I'm wondering is it worth adding some of them to mathlib? Or maybe some of them already exists?

[Yaël Dillies]

The first one is docs#div_add_one. The second one should be called odd.pos and is true in a docs#canonically_ordered_comm_semiring.

[Patrick Johnson]

Ok, I may open a PR (except for the first lemma). Which of (n / 2 * 2 + 1 = n) and (n / 2 * 2 = n - 1) is preferred?

[Yaël Dillies]

The first

[Oliver Nash]

Yaël Dillies said:

The first one is docs#div_add_one. The second one should be called odd.pos and is true in a docs#canonically_ordered_comm_semiring.

I note we have docs#nat.odd_gt_zero which is badly named. Your PR could fix this too!

[Yaël Dillies]

And generalize it!

[Patrick Johnson]

The second one should be called odd.pos and is true in a docs#canonically_ordered_comm_semiring.

It doesn't seem to be true in any canonically ordered commutative semiring. I guess I need a nontrivial instance. Do I need some more instances on it?

[Yaël Dillies]

None I think

[Yaël Dillies]

Ah yes, you need docs#nontrivial

[Ruben Van de Velde]

Maybe odd.ne_zero would also be useful