Skip to content

Commit

Permalink
[Imo1989P5] add missing copyright header
Browse files Browse the repository at this point in the history
  • Loading branch information
dwrensha committed Dec 9, 2023
1 parent 2581bb7 commit 271c68b
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions Compfiles/Imo1989P5.lean
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
/-
Copyright (c) 2023 David Renshaw. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Renshaw
-/

import Mathlib.Algebra.IsPrimePow
import Mathlib.Data.Nat.ModEq
import Mathlib.Data.Nat.Prime
Expand Down

0 comments on commit 271c68b

Please sign in to comment.