Finding out the Natural Language of a theorem in Mathlib

Stream: new members

[Jack Heseltine]

I am specifically wondering what this theorem means, but new to Mathlib and not googling successfully at the moment. Can someone point me to the correct way to find out about a question like this?

theorem prime . dvd_of_dvd _pow {p m n : ℕ} (pp : prime p) (h : p \[Divides] m^n) : p \[Divides] m :=
begin
induction n with n IH,
{ exact pp . not_dvd_one . elim h },
{ rw pow_succ at h, exact (pp . dvd_mul.1 h) . elim id IH }
end

[Kevin Buzzard]

It means that if $p$ is prime and $p|m^n$ then $p|m.$

[Scott Morrison]

@Jack Heseltine, there's not a general method for getting help with "what is the natural language version of this statement", beyond learning the basic Lean syntax so you can do it yourself, or asking here.

[Scott Morrison]

#3808 is a PR proposing a helper function for the opposite direction (i.e. a #formalize command), but it will only be useful for people either with GPT API access, or a locally running LLM. We could very easily add the other direction, as well.

[Johan Commelin]

Where does the \[Divides] syntax come from?

[Scott Morrison]

I think this text has been copied and pasted via Mathematica.

[Scott Morrison]

It rewrites Unicode in interesting ways (and is also prone to insert spaces around punctuation!)

[Kevin Buzzard]

import Mathlib.Tactic

namespace Nat

theorem prime.dvd_of_dvd_pow {p m n : ℕ} (pp : Prime p) (h : p ∣ m^n) : p ∣ m := by
  induction' n with n IH
  { exact pp.not_dvd_one.elim h }
  { rw [pow_succ] at h; exact (pp.dvd_mul.1 h).elim IH id }
  done

is something which you can just cut and paste into Lean 4.

[Alex Kontorovich]

If you have ChatGPT, you can get a much quicker answer by asking it directly (no guarantee that what it's saying is right, but it might give some useful hints). E.g.:
image.png