Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-09 11:19 fa28a8c5

View on Github →

feat(data/nat/parity): even/odd.mul_even/odd (#6584) Lemmas pertaining to the multiplication of even and odd natural numbers.

Estimated changes

added theorem nat.even.mul_left
added theorem nat.even.mul_right
modified theorem nat.even_div
added theorem nat.odd.mul
added theorem nat.odd.of_mul_left
added theorem nat.odd.of_mul_right
added theorem nat.odd_mul