feat(number_theory/divisors): mem_divisors_self (#10359)

From flt-regular. Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
leanprover-community · Nov 16, 2021 · bce0ede · bce0ede
1 parent 8f7971a
commit bce0ede
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/number_theory/divisors.lean b/src/number_theory/divisors.lean
@@ -91,6 +91,8 @@ begin
     apply nat.le_of_dvd (nat.succ_pos m) hdvd }
 end
 
+lemma mem_divisors_self (n : ℕ) (h : n ≠ 0) : n ∈ n.divisors := mem_divisors.2 ⟨dvd_rfl, h⟩
+
 lemma dvd_of_mem_divisors {m : ℕ} (h : n ∈ divisors m) : n ∣ m :=
 begin
   cases m,