better doc

leanprover-community · Sep 11, 2024 · 1988fda · 1988fda
1 parent fe3c43b
commit 1988fda
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
@@ -40,7 +40,7 @@ noncomputable
 def systemOfUnits.index [Module A G] (sys : systemOfUnits p G r) [sys.IsMaximal] :=
   Fintype.card (G ⧸ Submodule.span A (Set.range sys.units))
 
-/-- A system of units is fundamental if its maximal and has smallest index -/
+/-- A system of units is fundamental if it's maximal and the submodule generated by the elements of the system has smallest index. -/
 def systemOfUnits.IsFundamental [Module A G] (h : systemOfUnits p G r) :=
   ∃ _ : h.IsMaximal, ∀ (s : systemOfUnits p G r) (_ : s.IsMaximal), h.index ≤ s.index