From 1559f5acb49b8413fcd5eaa1a4768d5fb309b5d4 Mon Sep 17 00:00:00 2001
From: Hu Yongle <2065545849@qq.com>
Date: Sat, 26 Oct 2024 16:43:13 +0800
Subject: [PATCH] fix build

---
 GaloisRamification/GaloisRamification.lean            | 4 ++--
 GaloisRamification/Hilbert's_Ramification_Theory.lean | 2 +-
 lakefile.lean                                         | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/GaloisRamification/GaloisRamification.lean b/GaloisRamification/GaloisRamification.lean
index ab06f33..1b28349 100644
--- 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
index 7e58205..1f74a95 100644
--- 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
index 66735ef..fe0b4d1 100644
--- 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