Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-19 09:07 6f0c4fb3

View on Github →

feat(data/{int, nat}/parity): rename ne_of_odd_sum (#7261) ne_of_odd_sum becomes ne_of_odd_add.

Estimated changes

Modified archive/imo/imo1998_q2.lean

Modified src/data/int/parity.lean

added theorem int.ne_of_odd_add

deleted theorem int.ne_of_odd_sum

Modified src/data/nat/parity.lean

added theorem nat.ne_of_odd_add

deleted theorem nat.ne_of_odd_sum