Review of simple proof

Stream: new members

[Dylan]

Hi everyone! I'm just getting started with lean and trying to learn by implementing some simple proofs from my elementary number theory book. I'd appreciate any feedback on this proof or any advice for improving my code quality and conciseness.

Here's the theorem I proved:
SCR-20250107-tyla.png
SCR-20250107-tyoj.png

[Mitchell Lee]

Nice!

There shouldn't be any need to have any assumption like 0 < a ∧ ¬p ∣ a. The fact that ¬p ∣ a already implies that 0 < a. Also, it's usually considered better to write any assumption of the form P ∧ Q as two separate assumptions.

Your lemma order_one_mod_p shouldn't require either the assumption that p is prime or the assumption that 0 < a ∧ ¬p ∣ a. This is one of the benefits of providing the sensible junk value 0 as you did.

You can make your code a little simpler by making a and p implicit arguments to some of your lemmas. For example:

lemma order_gt_zero {a p : ℕ} (ha : 0 < a ∧ ¬p ∣ a) (hp : Prime p) : a.order p > 0 := by

This means you won't have to supply a and p when citing this lemma, because they can be inferred from the type of ha and hp.

[Mitchell Lee]

Great job with this proof. I recommend taking a look at Mathematics in Lean (https://leanprover-community.github.io/mathematics_in_lean/) if you haven't already.

[Dylan]

Thank you for the advice! I didn't realize how powerful implicit arguments are. I also managed to substantially simplify the proof using the calc tactic.