From 5ff452b9293377d66b7a64cf63ec9ef393e5a991 Mon Sep 17 00:00:00 2001 From: erd1 Date: Fri, 1 Dec 2023 12:15:34 +0800 Subject: [PATCH] fix? --- FltRegular/CaseII/Statement.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FltRegular/CaseII/Statement.lean b/FltRegular/CaseII/Statement.lean index 24e7e79d..7da16bed 100644 --- a/FltRegular/CaseII/Statement.lean +++ b/FltRegular/CaseII/Statement.lean @@ -55,7 +55,7 @@ lemma not_exists_Int_solution {p : ℕ} [hpri : Fact (Nat.Prime p)] (hreg : IsRe ℚ (B := (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)) (Set.mem_singleton (⟨p, hpri.out.pos⟩ : ℕ+)) have hodd' : (⟨p, hpri.out.pos⟩ : ℕ+) ≠ (2 : ℕ+) := by rwa [← PNat.coe_injective.ne_iff] - have := λ n ↦ zeta_sub_one_dvd_Int_iff (K := CyclotomicField ⟨p, hpri.out.pos⟩ ℚ) hζ hodd' (n := n) + have := fun n ↦ zeta_sub_one_dvd_Int_iff (K := CyclotomicField ⟨p, hpri.out.pos⟩ ℚ) hζ (n := n) simp only [PNat.mk_coe] at this simp_rw [← this] rintro ⟨x, y, z, hy, hz, hz', e⟩