Skip to content

Commit

Permalink
useless
Browse files Browse the repository at this point in the history
  • Loading branch information
riccardobrasca committed Nov 30, 2023
1 parent d208e82 commit 791cce6
Showing 1 changed file with 1 addition and 4 deletions.
5 changes: 1 addition & 4 deletions FltRegular/NumberTheory/SystemOfUnits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,6 @@ lemma Submodule.mem_stabilizer_span {R M} (S)
· intros _ _ h₁ h₂; rw [smul_add]; exact add_mem h₁ h₂
· intros r m h; rw [smul_comm]; exact Submodule.smul_mem _ r h

set_option synthInstance.maxHeartbeats 0 in
lemma mem_spanS [Module A G] {R : ℕ} {g : G} (a : A) (f : Fin R → G)
(hg : g ∈ Submodule.span ℤ
(Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p)^e.2.1 • f e.1))) :
Expand Down Expand Up @@ -133,18 +132,16 @@ lemma ex_not_mem [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) :
by_contra' h
sorry

set_option synthInstance.maxHeartbeats 0 in
lemma existence' [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) :
Nonempty (systemOfUnits p G (R + 1)) := by
obtain ⟨g, hg⟩ := ex_not_mem p G r S hR
refine ⟨⟨Fin.cases g S.units, ?_⟩⟩
refine LinearIndependent.fin_cons' g S.units S.linearIndependent (fun a y hy ↦ ?_)
by_contra' ha
letI := Fact.mk hp
obtain ⟨n, hn, f, Hf⟩ := CyclotomicIntegers.exists_dvd_int p _ ha
obtain ⟨n, _, f, Hf⟩ := CyclotomicIntegers.exists_dvd_int p _ ha
replace hy := congr_arg (f • ·) hy
simp only at hy
let mon : Monoid A := inferInstance
rw [smul_zero, smul_add, smul_smul, mul_comm f,
← Hf, ← eq_neg_iff_add_eq_zero, intCast_smul] at hy
apply hg n
Expand Down

0 comments on commit 791cce6

Please sign in to comment.