Theorem Nat.one_lt_of_ne_zero_of_even

Modification history

2025-07-31 03:42
Mathlib/Algebra/Group/Nat/Even.lean
feat: use grind in Nat/Int parity results (#27661)
Modified Nat.one_lt_of_ne_zero_of_evenView on Github →
2024-12-16 01:07
Mathlib/Algebra/Group/Nat/Even.lean
chore(Algebra/Group/Nat): Remove some unnecessary lemmas arguments (#19981)
Modified Nat.one_lt_of_ne_zero_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.one_lt_of_ne_zero_of_evenView on Github →