chore(data/nat): rename oddly named lemma odd_gt_zero (#13040)

leanprover-community · Jul 7, 2022 · ab99fd1 · ab99fd1
1 parent 6d02dac
commit ab99fd1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/archive/imo/imo1998_q2.lean b/archive/imo/imo1998_q2.lean
@@ -201,7 +201,7 @@ theorem imo1998_q2 [fintype J] [fintype C]
   (hk : ∀ (p : judge_pair J), p.distinct → (agreed_contestants r p).card ≤ k) :
   (b - 1) / (2 * b) ≤ k / a :=
 begin
-  rw clear_denominators ha (nat.odd_gt_zero hb),
+  rw clear_denominators ha (nat.pos_of_odd hb),
   obtain ⟨z, hz⟩ := hb, rw hz at hJ, rw hz,
   have h := le_trans (A_card_lower_bound r hJ) (A_card_upper_bound r hk),
   rw [hC, hJ] at h,

diff --git a/src/data/nat/parity.lean b/src/data/nat/parity.lean
@@ -72,7 +72,7 @@ begin
               one_ne_zero, and_self] },
 end
 
-lemma odd_gt_zero (h : odd n) : 0 < n :=
+lemma pos_of_odd (h : odd n) : 0 < n :=
 by { obtain ⟨k, rfl⟩ := h, exact succ_pos' }
 
 @[simp] theorem two_dvd_ne_zero : ¬ 2 ∣ n ↔ n % 2 = 1 :=