nat divisors

Stream: new members

[Alex Kontorovich]

Something very stupid; maybe someone can do it immediately:

lemma nat.divisors_eq (n y : ℕ) (hny : n ≤ y) :
  n.divisors = (finset.filter (λ (x : ℕ), x ∣ n) (finset.Icc 1 y)) :=
begin
  sorry,
end

This is nearly the definition of nat.divisor, except the finset.Icc goes from 1 to y instead of 1 to n. Since n≤ y and nat.divisor_le knows that any divisor is anyway less than n, these sets are the "same"...?

[Yakov Pechersky]

Not true for n = 0 :anguished:

[Alex Kontorovich]

Ok, let's add 0<n

[Yakov Pechersky]

import number_theory.divisors

lemma nat.divisors_eq (n y : ℕ) (hny : n ≤ y) :
  n.divisors = (finset.filter (λ (x : ℕ), x ∣ n) (finset.Icc 1 y)) :=
begin
  cases n,
  sorry, -- skip n = 0
  ext (_|a),
  { simp },
  suffices : a.succ ∣ n.succ → a.succ ≤ y,
  { simpa [and_comm, nat.succ_le_succ_iff] },
  exact λ h, (nat.le_of_dvd (nat.zero_lt_succ _) h).trans hny
end

[Alex Kontorovich]

Cool! What is that first line ext (_|a) doing? (I mean, I can see what it did in this case, but how do those parentheses work?...) Many thanks!

[Kyle Miller]

It does tactic#rcases on the introduced variables (a feature I was unaware of). The pipe pattern does cases on constructors of an inductive type.