Commit 2024-12-16 01:07 d3319caa

View on Github →

chore(Algebra/Group/Nat): Remove some unnecessary lemmas arguments (#19981)

Estimated changes

Modified Mathlib/Algebra/Group/Nat/Even.lean

modified theorem Nat.add_one_lt_of_even

modified theorem Nat.one_lt_of_ne_zero_of_even

modified theorem Nat.succ_mod_two_eq_one_iff

modified theorem Nat.succ_mod_two_eq_zero_iff