From bdbbe4576d5ca7674dc8ff3c573b9dfc0259fefc Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed, 31 Jan 2024 15:30:54 +0100 Subject: [PATCH] bump --- FltRegular/CaseII/AuxLemmas.lean | 5 ++--- FltRegular/CaseII/InductionStep.lean | 8 ++++---- FltRegular/NumberTheory/AuxLemmas.lean | 11 ----------- FltRegular/NumberTheory/Different.lean | 5 ++--- FltRegular/NumberTheory/GaloisPrime.lean | 4 ++-- FltRegular/NumberTheory/Hilbert92.lean | 9 ++++----- FltRegular/NumberTheory/KummersLemma/Field.lean | 9 +++++---- lake-manifest.json | 4 ++-- 8 files changed, 21 insertions(+), 34 deletions(-) diff --git a/FltRegular/CaseII/AuxLemmas.lean b/FltRegular/CaseII/AuxLemmas.lean index 19fb152e..ac0c9d4f 100644 --- a/FltRegular/CaseII/AuxLemmas.lean +++ b/FltRegular/CaseII/AuxLemmas.lean @@ -117,9 +117,8 @@ lemma pow_dvd_pow_iff_dvd {M : Type*} [CancelCommMonoidWithZero M] [UniqueFactor {a b : M} {x : ℕ} (h' : x ≠ 0) : a ^ x ∣ b ^ x ↔ a ∣ b := by classical by_cases ha : a = 0 - · rw [ha, zero_pow (Nat.pos_iff_ne_zero.mpr h'), zero_dvd_iff, zero_dvd_iff, - pow_eq_zero_iff (Nat.pos_iff_ne_zero.mpr h')] - have ha' : a ^ x ≠ 0 := (pow_eq_zero_iff (Nat.pos_iff_ne_zero.mpr h')).not.mpr ha + · rw [ha, zero_pow h', zero_dvd_iff, zero_dvd_iff, pow_eq_zero_iff h'] + have ha' : a ^ x ≠ 0 := (pow_ne_zero_iff h').mpr ha rw [dvd_iff_multiplicity_le ha, dvd_iff_multiplicity_le ha'] refine forall₂_congr (fun p hp ↦ ?_) simp_rw [multiplicity.pow hp, ← PartENat.withTopEquiv_le] diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean index 79b4207d..1eb24f4b 100644 --- a/FltRegular/CaseII/InductionStep.lean +++ b/FltRegular/CaseII/InductionStep.lean @@ -224,8 +224,8 @@ lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = ( Finset.prod_mul_distrib, Finset.prod_const, Finset.card_attach, hζ.unit'_coe.card_nthRootsFinset] at e' rw [← mul_right_inj' - ((pow_ne_zero_iff hpri.out.pos).mpr (m_ne_zero hζ e hy) : _), - ← mul_left_inj' ((pow_ne_zero_iff hpri.out.pos).mpr (p_ne_zero hζ) : _), e', + ((pow_ne_zero_iff hpri.out.ne_zero).mpr (m_ne_zero hζ e hy) : _), + ← mul_left_inj' ((pow_ne_zero_iff hpri.out.ne_zero).mpr (p_ne_zero hζ) : _), e', exists_ideal_pow_eq_c_aux] lemma exists_ideal_pow_eq_c : ∃ I : Ideal (𝓞 K), (𝔠 η) = I ^ (p : ℕ) := by @@ -437,8 +437,8 @@ lemma x_plus_y_mul_ne_zero : x + y * η ≠ 0 := by simp_rw [mul_comm _ y] exact Finset.dvd_prod_of_mem _ η.prop rw [hη, zero_dvd_iff, e] at this - simp only [mul_eq_zero, Units.ne_zero, PNat.pos, - pow_eq_zero_iff, add_pos_iff, or_true, false_or] at this + simp only [mul_eq_zero, Units.ne_zero, pow_eq_zero_iff p.ne_zero, add_pos_iff, or_true, false_or] + at this rw [this.resolve_left (pow_ne_zero (m + 1) (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt))] at hz exact hz (dvd_zero _) diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index b5cd7a13..a3817457 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/FltRegular/NumberTheory/AuxLemmas.lean @@ -10,17 +10,6 @@ This file contains lemmas that should go somewhere in a file in mathlib. -/ open BigOperators UniqueFactorizationMonoid --- Mathlib/RingTheory/DedekindDomain/Ideal.lean -lemma Ideal.mem_normalizedFactors_iff {R} [CommRing R] [IsDedekindDomain R] [DecidableEq (Ideal R)] - {p I : Ideal R} (hI : I ≠ ⊥) : - p ∈ normalizedFactors I ↔ p.IsPrime ∧ I ≤ p := by - rw [← Ideal.dvd_iff_le] - by_cases hp : p = 0 - · simp only [hp, zero_not_mem_normalizedFactors, isUnit_zero_iff, one_eq_top, zero_dvd_iff, - false_iff, not_and] - exact fun _ ↦ hI - · rwa [UniqueFactorizationMonoid.mem_normalizedFactors_iff hI, prime_iff_isPrime] - -- Mathlib/RingTheory/Ideal/Operations.lean lemma Ideal.comap_coe {R S F : Type*} [Semiring R] [Semiring S] [RingHomClass F R S] (f : F) (I : Ideal S) : I.comap (f : R →+* S) = I.comap f := rfl diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean index b23d0b70..69090244 100644 --- a/FltRegular/NumberTheory/Different.lean +++ b/FltRegular/NumberTheory/Different.lean @@ -36,7 +36,7 @@ variable [IsDedekindDomain A] [IsDedekindDomain B] [IsFractionRing B L] lemma pow_sub_one_dvd_differentIdeal_aux [NoZeroSMulDivisors A B] [Module.Finite A B] - {p : Ideal A} [p.IsMaximal] (P : Ideal B) (e : ℕ) (he : 0 < e) (hp : p ≠ ⊥) + {p : Ideal A} [p.IsMaximal] (P : Ideal B) (e : ℕ) (he : e ≠ 0) (hp : p ≠ ⊥) (hP : P ^ e ∣ p.map (algebraMap A B)) : P ^ (e - 1) ∣ differentIdeal A B := by obtain ⟨a, ha⟩ := (pow_dvd_pow _ (Nat.sub_le e 1)).trans hP have hp' := (Ideal.map_eq_bot_iff_of_injective @@ -50,7 +50,7 @@ lemma pow_sub_one_dvd_differentIdeal_aux apply_fun (· ^ e : Ideal B → _) at ha apply_fun (· ^ (e - 1) : Ideal B → _) at hb simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb - conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he.ne.symm)] + conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)] rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha exact ⟨_, ha.symm⟩ suffices : ∀ x ∈ a, Algebra.intTrace A B x ∈ p @@ -100,5 +100,4 @@ lemma pow_sub_one_dvd_differentIdeal Module.Finite_of_isLocalization A B _ _ A⁰ by_cases he : e = 0 · rw [he, pow_zero]; exact one_dvd _ - rw [← Ne.def, ← Nat.pos_iff_ne_zero] at he exact pow_sub_one_dvd_differentIdeal_aux A (FractionRing A) (FractionRing B) B P e he hp hP diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean index 0c9ff369..113485c7 100644 --- a/FltRegular/NumberTheory/GaloisPrime.lean +++ b/FltRegular/NumberTheory/GaloisPrime.lean @@ -364,11 +364,11 @@ lemma prod_smul_primesOver [IsGalois K L] (p : Ideal R) (P : primesOver S p) [p. Ideal.comap_bot_of_injective _ (galRestrict R K L S _).injective, Finset.prod_const, Ideal.map_bot, Ideal.inertiaDegIn_bot R S (IsIntegralClosure.isIntegral_algebra R L)] refine (zero_pow ?_).trans (zero_pow ?_).symm - · rw [pos_iff_ne_zero, Finset.card_univ, Ne.def, Fintype.card_eq_zero_iff] + · rw [Finset.card_univ, Ne.def, Fintype.card_eq_zero_iff] simp only [not_isEmpty_of_nonempty, not_false_eq_true] · have hR := not_imp_not.mp (Ring.ne_bot_of_isMaximal_of_not_isField ‹_›) rfl letI : Field R := hR.toField - exact finrank_pos + exact finrank_pos.ne' rw [← prod_primesOverFinset_pow_ramificationIdxIn K L p hp] delta Finset.prod rw [← pow_mul, ← Multiset.prod_nsmul, Multiset.map_id'] diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 4d9c9c9b..1211b9a4 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -784,11 +784,10 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E / conv => enter [1, 2, i] rw [h1 i, mul_comm] - rw [prod_mul_distrib, prod_const, card_range, prod_pow_eq_pow_sum] - simp only [inv_pow, ne_eq, PNat.pos, pow_eq_zero_iff, ZeroMemClass.coe_eq_zero, Units.ne_zero, - not_false_eq_true, mul_eq_left₀, inv_eq_one] - rw [sum_range_id, Nat.mul_div_assoc, pow_mul, ← map_pow, hζ, map_one, one_pow] - exact even_iff_two_dvd.1 (hp.even_sub_one hpodd) + rw [prod_mul_distrib, prod_const, card_range, prod_pow_eq_pow_sum, inv_pow, mul_eq_left₀, + inv_eq_one, sum_range_id, Nat.mul_div_assoc, pow_mul, ← map_pow, hζ, map_one, one_pow] + · exact even_iff_two_dvd.1 (hp.even_sub_one hpodd) + · simp attribute [-instance] instDecidableEq Fintype.decidableForallFintype diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean index 5c2f752c..4bd6381f 100644 --- a/FltRegular/NumberTheory/KummersLemma/Field.lean +++ b/FltRegular/NumberTheory/KummersLemma/Field.lean @@ -108,15 +108,16 @@ theorem aeval_poly {L : Type*} [Field L] [Algebra K L] (α : L) aeval (((1 : L) - ζ ^ m • α) / (algebraMap K L (ζ - 1))) (poly hp hζ u hcong) = 0 := by have hζ' : algebraMap K L ζ - 1 ≠ 0 · simpa using (algebraMap K L).injective.ne (hζ.sub_one_ne_zero hpri.out.one_lt) + rw [map_sub, map_one] have := congr_arg (aeval ((1 - ζ ^ m • α) / (algebraMap K L (ζ - 1)))) (poly_spec hp hζ u hcong) simp only [map_sub, map_one, map_pow, map_mul, aeval_C, Subalgebra.algebraMap_eq, smul_pow, RingHom.coe_comp, RingHom.coe_coe, Subalgebra.coe_val, Function.comp_apply, e, IsPrimitiveRoot.val_unit'_coe, map_add, aeval_X, ← mul_div_assoc, mul_div_cancel_left _ hζ', sub_sub_cancel_left, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow] at this - rw [← pow_mul, mul_comm m, pow_mul, hζ.pow_eq_one, one_pow, one_smul] at this - simp only [add_left_neg, mul_eq_zero, PNat.pos, pow_eq_zero_iff, hζ', false_or] at this - simpa only [map_sub, map_one] using this + rw [← pow_mul, mul_comm m, pow_mul, hζ.pow_eq_one, one_pow, one_smul, add_left_neg, + mul_eq_zero] at this + exact this.resolve_left (pow_ne_zero _ hζ') def polyRoot {L : Type*} [Field L] [Algebra K L] (α : L) (e : α ^ (p : ℕ) = algebraMap K L u) (m : ℕ) : 𝓞 L := @@ -130,7 +131,7 @@ theorem roots_poly {L : Type*} [Field L] [Algebra K L] (α : L) (Finset.range (p : ℕ)).val.map (fun i ↦ ((1 : L) - ζ ^ i • α) / (algebraMap K L (ζ - 1))) := by by_cases hα : α = 0 - · rw [hα, zero_pow p.pos] at e + · rw [hα, zero_pow p.ne_zero] at e exact (((algebraMap (𝓞 K) L).isUnit_map u.isUnit).ne_zero e.symm).elim have hζ' : algebraMap K L ζ - 1 ≠ 0 · simpa using (algebraMap K L).injective.ne (hζ.sub_one_ne_zero hpri.out.one_lt) diff --git a/lake-manifest.json b/lake-manifest.json index f092f726..383e6945 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096", + "rev": "a11bdfc39e95fa5b09e06638a43bd8bd2eddce12", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "cea4f7aabfdbf6d0967d580d38017fb0469b84b9", + "rev": "fdcd4ee3a122bf44fc58dc912fb5243ea4fe8916", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,