From d208e82f06c72a6237d6ecdb9525551a75410082 Mon Sep 17 00:00:00 2001
From: erd1 <the.erd.one@gmail.com>
Date: Fri, 1 Dec 2023 05:10:42 +0800
Subject: [PATCH] fix `spanA_eq_spanZ`

---
 FltRegular/NumberTheory/SystemOfUnits.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean
index 54d51b94..c61f127a 100644
--- a/FltRegular/NumberTheory/SystemOfUnits.lean
+++ b/FltRegular/NumberTheory/SystemOfUnits.lean
@@ -126,7 +126,7 @@ lemma spanA_eq_spanZ [Module A G] {R : ℕ} (f : Fin R → G) :
     · intro z w hz hw
       exact Submodule.add_mem _ hz hw
     · intro a _ hx
-      exact mem_spanS p G a f hx
+      exact mem_spanS p hp G _ f hx
 
 lemma ex_not_mem [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) :
         ∃ g, ∀ (k : ℤ), ¬(k • g ∈ Submodule.span A (Set.range S.units)) := by