@@ -252,6 +252,51 @@ section min_fac
252
252
end
253
253
end
254
254
255
+ /--
256
+ The square of the smallest prime factor of a composite number `n` is at most `n`.
257
+ -/
258
+ lemma min_fac_sq_le_self {n : ℕ} (w : 0 < n) (h : ¬ prime n) : (min_fac n)^2 ≤ n :=
259
+ have t : (min_fac n) ≤ (n/min_fac n) := min_fac_le_div w h,
260
+ calc
261
+ (min_fac n)^2 = (min_fac n) * (min_fac n) : pow_two (min_fac n)
262
+ ... ≤ (n/min_fac n) * (min_fac n) : mul_le_mul_right (min_fac n) t
263
+ ... ≤ n : div_mul_le_self n (min_fac n)
264
+
265
+ @[simp]
266
+ lemma min_fac_eq_one_iff {n : ℕ} : min_fac n = 1 ↔ n = 1 :=
267
+ begin
268
+ split,
269
+ { intro h,
270
+ by_contradiction,
271
+ have := min_fac_prime a,
272
+ rw h at this ,
273
+ exact not_prime_one this , },
274
+ { rintro rfl, refl, }
275
+ end
276
+
277
+ @[simp]
278
+ lemma min_fac_eq_two_iff (n : ℕ) : min_fac n = 2 ↔ 2 ∣ n :=
279
+ begin
280
+ split,
281
+ { intro h,
282
+ convert min_fac_dvd _,
283
+ rw h, },
284
+ { intro h,
285
+ have ub := min_fac_le_of_dvd (le_refl 2 ) h,
286
+ have lb := min_fac_pos n,
287
+ -- If `interval_cases` and `norm_num` were already available here,
288
+ -- this would be easy and pleasant.
289
+ -- But they aren't, so it isn't.
290
+ cases h : n.min_fac with m,
291
+ { rw h at lb, cases lb, },
292
+ { cases m with m,
293
+ { simp at h, subst h, cases h with n h, cases n; cases h, },
294
+ { cases m with m,
295
+ { refl, },
296
+ { rw h at ub,
297
+ cases ub with _ ub, cases ub with _ ub, cases ub, } } } }
298
+ end
299
+
255
300
end min_fac
256
301
257
302
theorem exists_dvd_of_not_prime {n : ℕ} (n2 : 2 ≤ n) (np : ¬ prime n) :
0 commit comments