From 74b236606bfc18fb8fcc77bce2b374c56fd075d7 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Fri, 4 Oct 2024 09:21:06 +0300 Subject: [PATCH 1/3] Proved `normal` --- FLT/MathlibExperiments/FrobeniusRiou.lean | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean index c63f6290..58fb4926 100644 --- a/FLT/MathlibExperiments/FrobeniusRiou.lean +++ b/FLT/MathlibExperiments/FrobeniusRiou.lean @@ -747,8 +747,21 @@ theorem algebraic {A : Type*} [CommRing A] {B : Type*} [Nontrivial B] [CommRing rw [eval_map, eval₂_hom, F_eval_eq_zero] exact algebraMap.coe_zero -theorem normal : Normal K L := by - sorry +include G in +theorem normal [DecidableEq L]: Normal K L := by + rw [normal_iff] + intro l + obtain ⟨f, hf⟩ := @f_exists G _ _ L _ K _ _ _ l + have hnz: f≠0 := by refine Monic.ne_zero_of_ne ?h.left.h ?h.left.hp; exact zero_ne_one' K; exact hf.1 + constructor + rw [← @isAlgebraic_iff_isIntegral] + unfold IsAlgebraic + use f + constructor + exact hnz + exact hf.2.2.1 + refine Polynomial.splits_of_splits_of_dvd (algebraMap K L) hnz hf.2.2.2 ?_ + apply minpoly.dvd; exact hf.2.2.1 open FiniteDimensional From 0875b28759ef2fc541ada3f2a4b3f8cff53edc25 Mon Sep 17 00:00:00 2001 From: Ahmad Alkhalawi <46321632+4hma4d@users.noreply.github.com> Date: Sun, 6 Oct 2024 16:07:19 +0300 Subject: [PATCH 2/3] Apply suggestions from code review Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> --- FLT/MathlibExperiments/FrobeniusRiou.lean | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean index 58fb4926..52de6562 100644 --- a/FLT/MathlibExperiments/FrobeniusRiou.lean +++ b/FLT/MathlibExperiments/FrobeniusRiou.lean @@ -748,20 +748,16 @@ theorem algebraic {A : Type*} [CommRing A] {B : Type*} [Nontrivial B] [CommRing exact algebraMap.coe_zero include G in -theorem normal [DecidableEq L]: Normal K L := by +theorem normal [DecidableEq L] : Normal K L := by rw [normal_iff] intro l - obtain ⟨f, hf⟩ := @f_exists G _ _ L _ K _ _ _ l - have hnz: f≠0 := by refine Monic.ne_zero_of_ne ?h.left.h ?h.left.hp; exact zero_ne_one' K; exact hf.1 + obtain ⟨f, hfmonic, _, hf, hfsplits⟩ := @f_exists G _ _ L _ K _ _ _ l + have hnz : f ≠ 0 := hfmonic.ne_zero constructor - rw [← @isAlgebraic_iff_isIntegral] - unfold IsAlgebraic - use f - constructor - exact hnz - exact hf.2.2.1 + · rw [← isAlgebraic_iff_isIntegral] + exact ⟨f, hfmonic.ne_zero, hf⟩ refine Polynomial.splits_of_splits_of_dvd (algebraMap K L) hnz hf.2.2.2 ?_ - apply minpoly.dvd; exact hf.2.2.1 + exact minpoly.dvd _ _ hf open FiniteDimensional From d25de036e1e2bffaee7cc09bf4da0fd85ab3d7f9 Mon Sep 17 00:00:00 2001 From: 4hma4d Date: Sun, 6 Oct 2024 17:08:11 +0300 Subject: [PATCH 3/3] Fixed proof --- FLT/MathlibExperiments/FrobeniusRiou.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean index 52de6562..378d2597 100644 --- a/FLT/MathlibExperiments/FrobeniusRiou.lean +++ b/FLT/MathlibExperiments/FrobeniusRiou.lean @@ -756,7 +756,7 @@ theorem normal [DecidableEq L] : Normal K L := by constructor · rw [← isAlgebraic_iff_isIntegral] exact ⟨f, hfmonic.ne_zero, hf⟩ - refine Polynomial.splits_of_splits_of_dvd (algebraMap K L) hnz hf.2.2.2 ?_ + refine Polynomial.splits_of_splits_of_dvd (algebraMap K L) hnz hfsplits ?_ exact minpoly.dvd _ _ hf open FiniteDimensional