Zulip Chat Archive
Stream: new members
Topic: norm_num for deciding primality?
Kevin Cheung (Sep 06 2024 at 18:50):
In the documentation https://github.com/leanprover-community/mathlib4/blob/24fce2d2db1a7ed39c8c5bdaf300d2ddfc83313f/Mathlib/Data/Nat/Prime/Defs.lean#L142-L142, there is this sentence: "If you need to prove that a particular number is prime, in any case you should not use by decide
, but rather by norm_num
, which is much faster."
However, I have the following and norm_num
is underlined with red squiggly line saying the goal is unsolved.
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Tactic.Normnum
example : Nat.Prime 3 := by decide
example : Nat.Prime 3 := by norm_num
Is there a more powerful version of norm_num
that needs to be imported? If so, what would that be?
Kyle Miller (Sep 06 2024 at 18:53):
Import Mathlib.Tactic.Normnum.Prime
, which has the norm num extension for primality.
Kevin Cheung (Sep 06 2024 at 18:53):
Thanks!
Kevin Cheung (Sep 06 2024 at 18:55):
Strange. When I perform a search for "Mathlib.Tactic.Normnum.Prime" at https://leanprover-community.github.io/mathlib4_docs/search.html?sitesearch=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib4_docs&q=mathlib.tactic.normnum.prime I got no results.
Ruben Van de Velde (Sep 06 2024 at 18:58):
It's a file
Kevin Cheung (Sep 06 2024 at 18:59):
I see. My bad.
Kyle Miller (Sep 06 2024 at 19:08):
It's worth browsing the Mathlib/Tactic/Normnum
folder to see what norm num plugins are available
Kevin Cheung (Sep 06 2024 at 19:14):
Thanks for the tip.
Last updated: May 02 2025 at 03:31 UTC