Skip to content

Commit

Permalink
bump
Browse files Browse the repository at this point in the history
riccardobrasca committed Mar 11, 2024
1 parent 3727a95 commit cafcac5
Showing 5 changed files with 25 additions and 24 deletions.
8 changes: 4 additions & 4 deletions FltRegular/CaseI/Statement.lean
Original file line number Diff line number Diff line change
@@ -238,10 +238,10 @@ theorem auxf' (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) :
exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5)
obtain ⟨i, hi⟩ := hcard
refine' ⟨i, sdiff_subset _ _ hi, _⟩
have hi0 : i ≠ 0 := fun h => by simp [h] at hi
have hi1 : i ≠ 1 := fun h => by simp [h] at hi
have hik₁ : i ≠ k₁ := fun h => by simp [h] at hi
have hik₂ : i ≠ k₂ := fun h => by simp [h] at hi
have hi0 : i ≠ 0 := fun h => by simp [h, s] at hi
have hi1 : i ≠ 1 := fun h => by simp [h, s] at hi
have hik₁ : i ≠ k₁ := fun h => by simp [h, s] at hi
have hik₂ : i ≠ k₂ := fun h => by simp [h, s] at hi
simp [f, hi0, hi1, hik₁, hik₂]

theorem auxf (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) : ∃ i : Fin p, f a b k₁ k₂ (i : ℕ) = 0 :=
16 changes: 8 additions & 8 deletions FltRegular/MayAssume/Lemmas.lean
Original file line number Diff line number Diff line change
@@ -27,24 +27,24 @@ theorem coprime {a b c : ℤ} {n : ℕ} (H : a ^ n + b ^ n = c ^ n) (hprod : a *
have hc : c ≠ 0 := fun hc => by simp [hc] at hprod
let s : Finset ℤ := {a, b, c}
set d : ℤ := s.gcd id
have hadiv : d ∣ a := gcd_dvd (by simp)
have hbdiv : d ∣ b := gcd_dvd (by simp)
have hcdiv : d ∣ c := gcd_dvd (by simp)
have hadiv : d ∣ a := gcd_dvd (by simp [s])
have hbdiv : d ∣ b := gcd_dvd (by simp [s])
have hcdiv : d ∣ c := gcd_dvd (by simp [s])
have hdzero : d ≠ 0 := fun hdzero => by
simpa [ha] using Finset.gcd_eq_zero_iff.1 hdzero a (by simp)
simpa [ha] using Finset.gcd_eq_zero_iff.1 hdzero a (by simp [s])
have hdp : d ^ n ≠ 0 := fun hdn => hdzero (pow_eq_zero hdn)
refine' ⟨_, _, fun habs => _⟩
· obtain ⟨na, hna⟩ := hadiv; obtain ⟨nb, hnb⟩ := hbdiv; obtain ⟨nc, hnc⟩ := hcdiv
rwa [← mul_left_inj' hdp, add_mul, ← mul_pow, ← mul_pow, ← mul_pow, hna, hnb, hnc,
Int.mul_ediv_cancel_left _ hdzero, Int.mul_ediv_cancel_left _ hdzero,
Int.mul_ediv_cancel_left _ hdzero, mul_comm, ← hna, mul_comm, ← hnb, mul_comm, ← hnc]
· simpa [gcd_eq_gcd_image] using
· simpa [gcd_eq_gcd_image, d] using
Finset.Int.gcd_div_id_eq_one (show a ∈ ({a, b, c} : Finset ℤ) by simp) ha
· simp only [mul_eq_zero] at habs
rcases habs with ((Ha | Hb) | Hc)
· exact ha (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp)) Ha)
· exact hb (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp)) Hb)
· exact hc (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp)) Hc)
· exact ha (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Ha)
· exact hb (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Hb)
· exact hc (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Hc)

end MayAssume

9 changes: 5 additions & 4 deletions FltRegular/NumberTheory/Hilbert92.lean
Original file line number Diff line number Diff line change
@@ -221,7 +221,7 @@ lemma corollary [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (a
← sum_add_distrib, Finsupp.total_apply, Finsupp.sum_fintype]
congr
· ext j
simp only [smul_smul, Finsupp.ofSupportFinite_coe, add_smul]
simp only [smul_smul, Finsupp.ofSupportFinite_coe, add_smul, b', b]
congr 1
· rw [mul_comm]
· rw [← intCast_smul (k := A), smul_smul]
@@ -871,9 +871,10 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) :
intro i
induction i using Fin.lastCases with
| last =>
simp only [Fin.snoc_last, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe]
simp only [Fin.snoc_last, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe, NE, η, H2]
| cast i =>
simp only [Fin.snoc_castSucc, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe]
simp only [Fin.snoc_castSucc, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe, NE,
η, H2, J, N, H]
· intro ε hε
refine hS.corollary p hp _ _ (finrank_G p hp hKL σ hσ) _ (ι ∘ Fin.castSucc) ?_ (mkG ε) ?_
· by_contra hε'
@@ -921,7 +922,7 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) :
Fin.sum_univ_castSucc]
simp only [Fin.snoc_castSucc, toMul_zsmul, unit_to_U_zpow, unitlifts_spec, Fin.snoc_last,
toMul_ofMul, RingHom.toMonoidHom_eq_coe, zpow_neg, unit_to_U_inv, Function.comp_apply,
unit_to_U_map, smul_zero, neg_zero, add_zero, add_right_eq_self]
unit_to_U_map, smul_zero, neg_zero, add_zero, add_right_eq_self, NE, η, H2, J, N, H]
apply_fun mkG at NE_p_pow
simp only [RingHom.toMonoidHom_eq_coe, unit_to_U_map,
unit_to_U_neg, unit_to_U_pow] at NE_p_pow
14 changes: 7 additions & 7 deletions lake-manifest.json
Original file line number Diff line number Diff line change
@@ -4,10 +4,10 @@
[{"url": "https://github.com/leanprover/std4",
"type": "git",
"subDir": null,
"rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
"rev": "ff9850c4726f6b9fb8d8e96980c3fcb2900be8bd",
"name": "std",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.6.0",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/quote4",
@@ -22,19 +22,19 @@
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
"rev": "056ca0fa8f5585539d0b940f532d9750c3a2270f",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.6.0",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"rev": "16cae05860b208925f54e5581ec5fd264823440c",
"rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.29",
"inputRev": "v0.0.30",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
@@ -58,7 +58,7 @@
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"rev": "1095e9af4d1f75960ab5485a6c5b3a851f48b5f4",
"rev": "f884087a041da7998696e87352f6f06e2e5f5713",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.6.0
leanprover/lean4:v4.7.0-rc2

0 comments on commit cafcac5

Please sign in to comment.