fix build

mbkybky · Oct 26, 2024 · 1559f5a · 1559f5a
1 parent 59700a1
commit 1559f5a
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/GaloisRamification/GaloisRamification.lean b/GaloisRamification/GaloisRamification.lean
@@ -14,9 +14,9 @@ set_option autoImplicit false
 
 /-!
 
-# Ramification theory in Galois extensions of number fields
+# Ramification theory in Galois extensions of Dedekind domains
 
-In this file, we discuss the ramification theory in Galois extensions of number fields, which is
+In this file, we discuss the ramification theory in Galois extensions of Dedekind domains, which is
   also called Hilbert's Ramification Theory.
 
 ## Main definitions and results

diff --git a/GaloisRamification/Hilbert's_Ramification_Theory.lean b/GaloisRamification/Hilbert's_Ramification_Theory.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Hu Yongle. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Hu Yongle
+Authors: Hu Yongle, Jiedong Jiang
 -/
 import Mathlib.Tactic
 import Mathlib.NumberTheory.NumberField.Norm

diff --git a/lakefile.lean b/lakefile.lean
@@ -7,11 +7,11 @@ package "GaloisRamification" where
     ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
   ]
   -- add any additional package configuration options here
-  version := v!"0.1.0"
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
+@[default_target]
 lean_lib «GaloisRamification» where
   -- add library configuration options here