Primes > 2 are odd

Stream: Is there code for X?

[Niels Voss]

Is there a version of this statement in mathlib?

lemma odd_of_prime_gt_two (p : ℕ) (h : nat.prime p) (hp : 2 < p) : odd p :=
begin
  rw [nat.odd_iff_not_even, even_iff_two_dvd],
  rw nat.prime_dvd_prime_iff_eq nat.prime_two h,
  exact ne_of_lt hp
end

This came up during my PR but I wasn't able to find it using library search.

[Johan Commelin]

I guess the closest we have is docs#nat.prime.eq_two_or_odd

[Kevin Buzzard]

I think that's the second closest -- the closest is docs#nat.prime.eq_two_or_odd'

[Kevin Buzzard]

lemma odd_of_prime_gt_two (p : ℕ) (h : nat.prime p) (hp : 2 < p) : odd p :=
or.resolve_left (h.eq_two_or_odd') hp.ne'

[Kevin Buzzard]

Makes me wonder whether eq_two_or_odd' is actually usable in the application rather than odd_of_prime_gt_two

[Eric Rodriguez]

there's docs#nat.prime.odd_of_ne_two, which used to be called docs#nat.prime.odd until naming people decided that this wasn't right

[Eric Rodriguez]

I personally think that "obvious" hypotheses shouldn't be in the theorem title, but :shrug:

[Niels Voss]

This lemma was actually added after I originally opened my pull request, so the version of mathlib that my code branched from is actually outdated. I think I'm going to try running a git merge.

[Niels Voss]

I ran git merge and there were no merge conflicts, but now the Lean window in VSCode is constantly loading. If I had to guess, it's probably building 360 commits worth of oleans. Is there a way I can download those instead of rebuilding them?

[Martin Dvořák]

Maybe leanproject get-mathlib-cache is what you want.

[Junyan Xu]

If you're working in mathlib rather than another Lean project, I'd recommend:
leanproject get-cache --rev <hash of latest mathlib commit>
then
lean --make <path to the file you want to work on>

[Niels Voss]

leanproject get-cache --rev a7aa4a2e6c (where a7aa4a2e6c is the most recent master commit) seemed to work
norm_num now fails in one case but that shouldn't be that hard to fix

[Niels Voss]

It seems to work now

[Yaël Dillies]

The way I get cache just after merging is leanproject get-c --rev origin/master

[Yaël Dillies]

You can also do leanproject get-c, see what commits leanproject gives you, and do leanproject get-c --rev the_first_one.

[Eric Wieser]

Or just do leanproject get-cache --fallback=download-first which does those two things for you