feat(Algebra/Ring/Parity): Add lemmas Odd.add_one and Odd.one_add (…

…#19272)
leanprover-community · Nov 21, 2024 · 1d199de · 1d199de
1 parent 1e5f38b
commit 1d199de
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean
@@ -113,6 +113,8 @@ lemma Odd.add_odd : Odd a → Odd b → Even (a + b) := by
 
 @[simp] lemma Even.add_one (h : Even a) : Odd (a + 1) := h.add_odd odd_one
 @[simp] lemma Even.one_add (h : Even a) : Odd (1 + a) := h.odd_add odd_one
+@[simp] lemma Odd.add_one (h : Odd a) : Even (a + 1) := h.add_odd odd_one
+@[simp] lemma Odd.one_add (h : Odd a) : Even (1 + a) := odd_one.add_odd h
 
 lemma odd_two_mul_add_one (a : α) : Odd (2 * a + 1) := ⟨_, rfl⟩