Update archimedean.lean

ChrisHughes24 · Apr 2, 2019 · 195d830 · 195d830
1 parent d313bc5
commit 195d830
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/algebra/archimedean.lean b/src/algebra/archimedean.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 
 Archimedean groups and fields.
 -/
+--hi
 import algebra.group_power algebra.field_power
 import data.rat tactic.linarith tactic.abel