Skip to content

Commit

Permalink
feat: mark Data.Nat.PrimeNormNum as ported (#4253)
Browse files Browse the repository at this point in the history
The `norm_num` extension was already ported in #3892, so this PR adopts the same approach as #3816.
  • Loading branch information
Parcly-Taxel committed May 23, 2023
1 parent c092497 commit 79617e9
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Expand Up @@ -1197,6 +1197,7 @@ import Mathlib.Data.Nat.Periodic
import Mathlib.Data.Nat.Pow
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Nat.PrimeFin
import Mathlib.Data.Nat.PrimeNormNum
import Mathlib.Data.Nat.Set
import Mathlib.Data.Nat.Size
import Mathlib.Data.Nat.Sqrt
Expand Down
23 changes: 23 additions & 0 deletions Mathlib/Data/Nat/PrimeNormNum.lean
@@ -0,0 +1,23 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
! This file was ported from Lean 3 source module data.nat.prime_norm_num
! leanprover-community/mathlib commit 10b4e499f43088dd3bb7b5796184ad5216648ab1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Factors
import Mathlib.Data.Nat.Prime
import Mathlib.Tactic.NormNum

/-!
# Primality prover
This file provides a `norm_num` extention to prove that natural numbers are prime.
Porting note: the sole purpose of this file is to mark it as "ported".
This file seems to be tripping up the porting dashboard.
-/

0 comments on commit 79617e9

Please sign in to comment.