Theorem Nat.add_one_lt_of_even

Modification history

2024-12-16 01:07
Mathlib/Algebra/Group/Nat/Even.lean
chore(Algebra/Group/Nat): Remove some unnecessary lemmas arguments (#19981)
Modified Nat.add_one_lt_of_evenView on Github →
2024-11-11 12:43
Mathlib/Algebra/Group/Nat.lean
feat(Data/Fin/Parity): add lemmas about parity of `Fin` numbers (#8960)
Added Nat.add_one_lt_of_evenView on Github →