From bce0ede7d4e3105008946d5b393748b93d228b49 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Tue, 16 Nov 2021 21:57:02 +0000
Subject: [PATCH] feat(number_theory/divisors): mem_divisors_self (#10359)

From flt-regular.



Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
---
 src/number_theory/divisors.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/number_theory/divisors.lean b/src/number_theory/divisors.lean
index 026aea13d66e4..80b32a28e0f2a 100644
--- 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,