From 7710008c0dc6528c8a72df122a9f692f51c70b5e Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 16 Nov 2023 20:38:41 +0100 Subject: [PATCH] bump --- FltRegular/CaseII/AuxLemmas.lean | 2 +- FltRegular/NumberTheory/AuxLemmas.lean | 40 ++++++++----------- .../NumberTheory/Cyclotomic/CyclRat.lean | 6 +-- .../Cyclotomic/CyclotomicUnits.lean | 2 +- .../Cyclotomic/GaloisActionOnCyclo.lean | 3 +- .../NumberTheory/Cyclotomic/UnitLemmas.lean | 5 +-- FltRegular/NumberTheory/Different.lean | 6 +-- FltRegular/NumberTheory/GaloisPrime.lean | 2 +- FltRegular/NumberTheory/IdealNorm.lean | 4 +- FltRegular/NumberTheory/KummerExtension.lean | 10 ++--- .../NumberTheory/KummersLemma/Field.lean | 4 +- .../KummersLemma/KummersLemma.lean | 4 +- FltRegular/NumberTheory/RegularPrimes.lean | 6 ++- .../ReadyForMathlib/Homogenization.lean | 1 - lake-manifest.json | 28 ++++++------- lean-toolchain | 2 +- 16 files changed, 56 insertions(+), 69 deletions(-) diff --git a/FltRegular/CaseII/AuxLemmas.lean b/FltRegular/CaseII/AuxLemmas.lean index 45d3c4f0..5deda380 100644 --- a/FltRegular/CaseII/AuxLemmas.lean +++ b/FltRegular/CaseII/AuxLemmas.lean @@ -139,7 +139,7 @@ theorem isPrincipal_of_isPrincipal_pow_of_Coprime' rw [← Ne.def, ← isUnit_iff_ne_zero] at Izero show Submodule.IsPrincipal (Izero.unit' : FractionalIdeal A⁰ K) rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff] - refine ⟨?_, orderOf_dvd_card_univ⟩ + refine ⟨?_, orderOf_dvd_card⟩ rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff] simp only [Units.val_pow_eq_pow_val, IsUnit.val_unit', hI] diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index 4a68165c..4d10e6aa 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/FltRegular/NumberTheory/AuxLemmas.lean @@ -53,23 +53,15 @@ lemma AlgEquiv.toAlgHom_toRingHom {R A₁ A₂} [CommSemiring R] [Semiring A₁] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = e := rfl --- Mathlib/Algebra/Algebra/Hom.lean -lemma AlgEquiv.toRingEquiv_toRingHom {R A₁ A₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] - [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ((e : A₁ ≃+* A₂) : A₁ →+* A₂) = e := - rfl - -- Mathlib/RingTheory/Localization/Away/Basic.lean -- Sounds like a bad place but this should go before `IsLocalization.atUnits`. lemma IsLocalization.at_units {R : Type*} [CommSemiring R] (S : Submonoid R) (hS : ∀ s : S, IsUnit (s : R)) : IsLocalization S R where map_units' := hS surj' := fun s ↦ ⟨⟨s, 1⟩, by simp⟩ - eq_iff_exists' := fun {x y} ↦ by - constructor - · rintro (rfl : x = y) - exact ⟨1, rfl⟩ - · rintro ⟨c, hc⟩ - exact (hS c).mul_left_cancel hc + exists_of_eq := fun {x y} ↦ by + rintro (rfl : x = y) + exact ⟨1, rfl⟩ -- Mathlib/RingTheory/Localization/FractionRing.lean instance {R : Type*} [Field R] : IsFractionRing R R := @@ -561,7 +553,7 @@ theorem IsIntegralClosure.isLocalization' (ha : Algebra.IsAlgebraic K L) [NoZero haveI : IsDomain C := (IsIntegralClosure.equiv A C L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L) haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L - refine' ⟨_, fun z => _, fun {x y} => ⟨fun h => ⟨1, _⟩, _⟩⟩ + refine' ⟨_, fun z => _, fun {x y} => fun h => ⟨1, _⟩⟩ · rintro ⟨_, x, hx, rfl⟩ rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L), Subtype.coe_mk, map_ne_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective A C)] @@ -574,10 +566,6 @@ theorem IsIntegralClosure.isLocalization' (ha : Algebra.IsAlgebraic K L) [NoZero rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def, smul_def] · simp only [IsIntegralClosure.algebraMap_injective C A L h] - · rintro ⟨⟨_, m, hm, rfl⟩, h⟩ - refine' congr_arg (algebraMap C L) ((mul_right_inj' _).mp h) - rw [Subtype.coe_mk, map_ne_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective A C)] - exact mem_nonZeroDivisors_iff_ne_zero.mp hm end -- Mathlib/RingTheory/Algebraic.lean @@ -652,13 +640,14 @@ lemma isAlgebraic_of_isFractionRing {R S} (K L) [CommRing R] [CommRing S] [Field intro x obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective S⁰ x rw [isAlgebraic_iff_isIntegral, IsLocalization.mk'_eq_mul_mk'_one] - apply isIntegral_mul + apply RingHom.is_integral_mul · apply isIntegral_of_isScalarTower (R := R) - apply map_isIntegral (IsScalarTower.toAlgHom R S L) + apply IsIntegral.map (IsScalarTower.toAlgHom R S L) exact h x - · rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral] + · show IsIntegral _ _ + rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral] apply isIntegral_of_isScalarTower (R := R) - apply map_isIntegral (IsScalarTower.toAlgHom R S L) + apply IsIntegral.map (IsScalarTower.toAlgHom R S L) exact h s -- Mathlib/RingTheory/IntegralClosure.lean @@ -669,7 +658,7 @@ lemma isIntegralClosure_of_isIntegrallyClosed (R S K) [CommRing R] [CommRing S] refine ⟨IsLocalization.injective _ le_rfl, fun {x} ↦ ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (isIntegral_of_isScalarTower (A := S) hx), ?_⟩⟩ rintro ⟨y, rfl⟩ - exact map_isIntegral (IsScalarTower.toAlgHom R S K) (hRS y) + exact IsIntegral.map (IsScalarTower.toAlgHom R S K) (hRS y) -- Mathlib/RingTheory/IntegralClosure.lean -- or Mathlib/RingTheory/LocalProperties.lean @@ -707,11 +696,14 @@ lemma IsIntegral_of_isLocalization (R S Rₚ Sₚ) [CommRing R] [CommRing S] [Co obtain ⟨x, ⟨_, t, ht, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid S M) x rw [IsLocalization.mk'_eq_mul_mk'_one] - apply isIntegral_mul - · exact isIntegral_of_isScalarTower (map_isIntegral (IsScalarTower.toAlgHom R S Sₚ) (hRS x)) - · convert isIntegral_algebraMap (x := IsLocalization.mk' Rₚ 1 ⟨t, ht⟩) + apply RingHom.is_integral_mul + · exact isIntegral_of_isScalarTower (IsIntegral.map (IsScalarTower.toAlgHom R S Sₚ) (hRS x)) + · show IsIntegral _ _ + convert isIntegral_algebraMap (x := IsLocalization.mk' Rₚ 1 ⟨t, ht⟩) rw [this, IsLocalization.map_mk', _root_.map_one] + + -- Mathlib/RingTheory/Polynomial/ScaleRoots.lean (this section is not needed anymore) section scaleRoots diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean index 027947a2..b7af9b8b 100644 --- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean +++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean @@ -174,8 +174,7 @@ theorem prim_coe (ζ : R) (hζ : IsPrimitiveRoot ζ p) : IsPrimitiveRoot (ζ : C theorem zeta_sub_one_dvb_p [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η : R} (hη : η ∈ nthRootsFinset p R) (hne1 : η ≠ 1) : 1 - η ∣ (p : R) := by - have h00 : 1 - η ∣ (p : R) ↔ η - 1 ∣ (p : R) := - by + have h00 : 1 - η ∣ (p : R) ↔ η - 1 ∣ (p : R) := by have hh : -(η - 1) = 1 - η := by ring simp_rw [← hh] apply neg_dvd @@ -192,7 +191,8 @@ theorem zeta_sub_one_dvb_p [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η : R} (hη : ext rw [RingOfIntegers.coe_algebraMap_norm] norm_cast at h2 - simp [h2] + rw [h2] + simp theorem one_sub_zeta_prime [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R) (hne1 : η ≠ 1) : Prime (1 - η) := by diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean b/FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean index 0379d596..9e47be5a 100644 --- a/FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean +++ b/FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean @@ -70,7 +70,7 @@ theorem associated_one_sub_pow_primitive_root_of_coprime {n j k : ℕ} {ζ : A} replace hn := Nat.one_lt_of_ne n hn' hn obtain ⟨m, hm⟩ := Nat.exists_mul_emod_eq_one_of_coprime hj hn use ∑ i in range m, (ζ ^ j) ^ i - have : ζ = (ζ ^ j) ^ m := by rw [← pow_mul, pow_eq_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one] + have : ζ = (ζ ^ j) ^ m := by rw [← pow_mul, ←pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one] nth_rw 1 [this] rw [← geom_sum_mul_neg, mul_comm] diff --git a/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean b/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean index 7b47bc2f..d5143a54 100644 --- a/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean +++ b/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean @@ -71,7 +71,6 @@ theorem embedding_conj (x : K) (φ : K →+* ℂ) : conj (φ x) = φ (galConj K suffices φ (galConj K p ζ) = conj (φ ζ) by rw [← Function.funext_iff] - dsimp only congr rw [FunLike.coe_fn_eq] apply (hζ.powerBasis ℚ).rat_hom_ext @@ -90,7 +89,7 @@ variable (p) --generalize this theorem gal_map_mem {x : K} (hx : x ∈ RR) (σ : K →ₐ[ℚ] K) : σ x ∈ RR := - map_isIntegral (σ.restrictScalars ℤ) hx + map_isIntegral_int (σ.restrictScalars ℤ) hx theorem gal_map_mem_subtype (σ : K →ₐ[ℚ] K) (x : RR) : σ x ∈ RR := by simp [gal_map_mem] diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean index 544cd8f4..0bf420a7 100644 --- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean @@ -77,8 +77,7 @@ theorem zeta_runity_pow_even (hpo : Odd (p : ℕ)) (n : ℕ) : variable [NumberField K] -theorem IsPrimitiveRoot.unit'_coe : IsPrimitiveRoot (hζ.unit' : R) p := - by +theorem IsPrimitiveRoot.unit'_coe : IsPrimitiveRoot (hζ.unit' : R) p := by have z1 := hζ have : (algebraMap R K) (hζ.unit' : R) = ζ := rfl rw [← this] at z1 @@ -415,7 +414,7 @@ theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u : Units.val_pow_eq_pow_val] at hz norm_cast at hz simpa [hz] using unit_inv_conj_not_neg_zeta_runity hζ h u n hp - · apply isIntegral_mul + · apply RingHom.is_integral_mul exact NumberField.RingOfIntegers.isIntegral_coe _ exact NumberField.RingOfIntegers.isIntegral_coe _ · exact unit_lemma_val_one p u diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean index 9f884af9..fb915e48 100644 --- a/FltRegular/NumberTheory/Different.lean +++ b/FltRegular/NumberTheory/Different.lean @@ -115,7 +115,7 @@ lemma isIntegral_discr_mul_of_mem_traceFormDualSubmodule apply IsIntegral.sum intro i _ rw [smul_mul_assoc, b.equivFun.map_smul, discr_def, mul_comm, ← H, Algebra.smul_def] - refine isIntegral_mul ?_ (hb _) + refine RingHom.is_integral_mul _ ?_ (hb _) apply IsIntegral.algebraMap rw [cramer_apply] apply IsIntegral.det @@ -128,7 +128,7 @@ lemma isIntegral_discr_mul_of_mem_traceFormDualSubmodule have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp (hb j) rw [mul_comm, ← hy, ← Algebra.smul_def] exact I.smul_mem _ (ha) - · exact isIntegral_trace (isIntegral_mul (hb j) (hb k)) + · exact isIntegral_trace (RingHom.is_integral_mul _ (hb j) (hb k)) variable (A K) @@ -427,7 +427,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] mem_coeIdeal_conductor] have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0 · rwa [ne_eq, inv_eq_zero] - have : IsIntegral A (algebraMap B L x) := map_isIntegral (IsScalarTower.toAlgHom A B L) hAx + have : IsIntegral A (algebraMap B L x) := IsIntegral.map (IsScalarTower.toAlgHom A B L) hAx simp_rw [← Subalgebra.mem_toSubmodule, ← Submodule.mul_mem_smul_iff (y := y * _) hne₂] rw [← traceFormDualSubmodule_span_adjoin A K L _ hx this] simp only [mem_traceFormDualSubmodule, traceForm_apply, Subalgebra.mem_toSubmodule, diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean index b7361211..f135444f 100644 --- a/FltRegular/NumberTheory/GaloisPrime.lean +++ b/FltRegular/NumberTheory/GaloisPrime.lean @@ -114,7 +114,7 @@ noncomputable def galRestrictHom : (L →ₐ[K] L) →* (S →ₐ[R] S) where toFun := fun f ↦ (IsIntegralClosure.equiv R (integralClosure R L) L S).toAlgHom.comp (((f.restrictScalars R).comp (IsScalarTower.toAlgHom R S L)).codRestrict - (integralClosure R L) (fun x ↦ map_isIntegral _ (IsIntegralClosure.isIntegral R L x))) + (integralClosure R L) (fun x ↦ IsIntegral.map _ (IsIntegralClosure.isIntegral R L x))) map_one' := by ext x apply (IsIntegralClosure.equiv R (integralClosure R L) L S).symm.injective diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean index 77f88105..d38ec9bb 100644 --- a/FltRegular/NumberTheory/IdealNorm.lean +++ b/FltRegular/NumberTheory/IdealNorm.lean @@ -40,7 +40,7 @@ def Algebra.intNormAux (R S K L) [CommRing R] [CommRing S] [Field K] [Field L] [IsFractionRing R K] [FiniteDimensional K L] [IsSeparable K L] : S →* R where toFun := fun s ↦ IsIntegralClosure.mk' (R := R) R (Algebra.norm K (algebraMap S L s)) - (isIntegral_norm K <| map_isIntegral (IsScalarTower.toAlgHom R S L) + (isIntegral_norm K <| IsIntegral.map (IsScalarTower.toAlgHom R S L) (IsIntegralClosure.isIntegral R L s)) map_one' := by simp map_mul' := fun x y ↦ by simpa using IsIntegralClosure.mk'_mul _ _ _ _ _ @@ -288,7 +288,7 @@ theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₘ) (A := Sₘ)) cases h : subsingleton_or_nontrivial R · haveI := IsLocalization.unique R Rₘ M - simp + simp only [eq_iff_true_of_subsingleton] rw [map_spanIntNorm] refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_) · rintro a' ha' diff --git a/FltRegular/NumberTheory/KummerExtension.lean b/FltRegular/NumberTheory/KummerExtension.lean index 0cbc276c..97a1d050 100644 --- a/FltRegular/NumberTheory/KummerExtension.lean +++ b/FltRegular/NumberTheory/KummerExtension.lean @@ -452,7 +452,7 @@ lemma minpoly_algEquiv_toLinearMap (σ : L ≃ₐ[K] L) : -- However `{ σⁱ }` are linear independent (via Dedekind's linear independence of characters). have := Fintype.linearIndependent_iff.mp ((linearIndependent_algEquiv_toLinearMap K L).comp _ - (Subtype.val_injective.comp (finEquivPowers σ).injective)) + (Subtype.val_injective.comp ((finEquivPowers σ (isOfFinOrder_of_finite σ)).injective))) ((minpoly K σ.toLinearMap).coeff ∘ (↑)) this ⟨_, H⟩ simpa using this @@ -500,15 +500,15 @@ lemma irreducible_X_pow_sub_C_of_root_adjoin_eq_top {a : K} {α : L} (ha : α ^ (finrank K L) = algebraMap K L a) (hα : K⟮α⟯ = ⊤) : Irreducible (X ^ (finrank K L) - C a) := by have : minpoly K α = X ^ (finrank K L) - C a - · apply eq_of_monic_of_associated (minpoly.monic (isIntegral_of_finite K α)) + · apply eq_of_monic_of_associated (minpoly.monic (IsIntegral.of_finite K α)) (monic_X_pow_sub_C _ finrank_pos.ne.symm) refine Polynomial.associated_of_dvd_of_natDegree_eq ?_ ?_ (X_pow_sub_C_ne_zero finrank_pos _) · refine minpoly.dvd _ _ ?_ simp only [aeval_def, eval₂_sub, eval₂_X_pow, ha, eval₂_C, sub_self] - · rw [← IntermediateField.adjoin.finrank (isIntegral_of_finite K α), hα, natDegree_X_pow_sub_C] + · rw [← IntermediateField.adjoin.finrank (IsIntegral.of_finite K α), hα, natDegree_X_pow_sub_C] exact finrank_top K L - exact this ▸ minpoly.irreducible (isIntegral_of_finite K α) + exact this ▸ minpoly.irreducible (IsIntegral.of_finite K α) lemma isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top {a : K} {α : L} (ha : α ^ (finrank K L) = algebraMap K L a) (hα : K⟮α⟯ = ⊤) : @@ -520,7 +520,7 @@ lemma isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top rw [mem_primitiveRoots finrank_pos] at hζ exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective) ha · rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← hα, - IntermediateField.adjoin_simple_toSubalgebra_of_integral (isIntegral_of_finite K α)] + IntermediateField.adjoin_simple_toSubalgebra_of_integral (IsIntegral.of_finite K α)] apply Algebra.adjoin_mono rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a), aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self] diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean index 05e9c16f..018cd9a2 100644 --- a/FltRegular/NumberTheory/KummersLemma/Field.lean +++ b/FltRegular/NumberTheory/KummersLemma/Field.lean @@ -7,8 +7,6 @@ import Mathlib.Data.Polynomial.Taylor open scoped NumberField BigOperators -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220 - variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] variable (hp : p ≠ 2) @@ -256,7 +254,7 @@ lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L) AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one, SubmonoidClass.coe_pow] at hv have hα : IsIntegral (𝓞 K) α - · apply isIntegral_of_pow p.pos; rw [e]; exact isIntegral_algebraMap + · apply IsIntegral.of_pow p.pos; rw [e]; exact isIntegral_algebraMap have : IsUnit (⟨α, isIntegral_trans (IsIntegralClosure.isIntegral_algebra ℤ K) _ hα⟩ : 𝓞 L) · rw [← isUnit_pow_iff p.pos.ne.symm] convert (algebraMap (𝓞 K) (𝓞 L)).isUnit_map u.isUnit diff --git a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean index 933a1aa8..dd301bcd 100644 --- a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean +++ b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean @@ -5,8 +5,6 @@ import FltRegular.NumberTheory.IdealNorm open scoped NumberField -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220 - variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] variable (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))] (hreg : (p : ℕ).Coprime <| Fintype.card <| ClassGroup (𝓞 K)) @@ -157,7 +155,7 @@ theorem eq_pow_prime_of_unit_of_congruent (u : (𝓞 K)ˣ) simp only [not_forall, not_not] at this obtain ⟨v, hv⟩ := this have hv' : IsIntegral ℤ v - · apply isIntegral_of_pow p.pos; rw [hv]; exact (u ^ (p - 1 : ℕ) : 𝓞 K).prop + · apply IsIntegral.of_pow p.pos; rw [hv]; exact (u ^ (p - 1 : ℕ) : 𝓞 K).prop have : IsUnit (⟨v, hv'⟩ : 𝓞 K) · rw [← isUnit_pow_iff p.pos.ne.symm]; convert (u ^ (p - 1 : ℕ) : (𝓞 K)ˣ).isUnit; ext; exact hv have hv'' : this.unit ^ (p : ℕ) = u ^ (p - 1 : ℕ) diff --git a/FltRegular/NumberTheory/RegularPrimes.lean b/FltRegular/NumberTheory/RegularPrimes.lean index a085d44c..9f6b1461 100644 --- a/FltRegular/NumberTheory/RegularPrimes.lean +++ b/FltRegular/NumberTheory/RegularPrimes.lean @@ -81,7 +81,9 @@ def cyclotomicFieldTwoEquiv [IsCyclotomicExtension {2} K L] : L ≃ₐ[K] K := b exact (IsSplittingField.algEquiv L (cyclotomic 2 K)).trans (IsSplittingField.algEquiv K <| cyclotomic 2 K).symm - exact ⟨by simpa using @splits_X_sub_C _ _ _ _ (RingHom.id K) (-1), by simp⟩ + exact ⟨by simpa using @splits_X_sub_C _ _ _ _ (RingHom.id K) (-1), + by simp [eq_iff_true_of_subsingleton]⟩ + instance IsPrincipalIdealRing_of_IsCyclotomicExtension_two (L : Type _) [Field L] [CharZero L] [IsCyclotomicExtension {2} ℚ L] : @@ -126,5 +128,5 @@ theorem IsPrincipal_of_IsPrincipal_pow_of_Coprime swap; · exact Izero swap; · exact pow_ne_zero p Izero rw [← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff] - refine ⟨?_, orderOf_dvd_card_univ⟩ + refine ⟨?_, orderOf_dvd_card⟩ rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow] diff --git a/FltRegular/ReadyForMathlib/Homogenization.lean b/FltRegular/ReadyForMathlib/Homogenization.lean index 53cfba6c..cd3f24d3 100644 --- a/FltRegular/ReadyForMathlib/Homogenization.lean +++ b/FltRegular/ReadyForMathlib/Homogenization.lean @@ -410,7 +410,6 @@ theorem exists_coeff_ne_zero_totalDegree {p : MvPolynomial ι R} (hp : p ≠ 0) constructor · rw [← totalDegree_eq p] at hb₂ rw [hb₂] - dsimp -- TODO break this out as a lemma exact (Finsupp.card_toMultiset _).symm diff --git a/lake-manifest.json b/lake-manifest.json index 08814003..a8c0f8f2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "5f066e77432aee5c14c229c3aaa178ff639be1a2", + "rev": "48237d43209009b253cafc0920ca4e0772c2aeac", "opts": {}, "name": "mathlib", "inputRev?": null, @@ -12,23 +12,15 @@ {"git": {"url": "https://github.com/leanprover/doc-gen4", "subDir?": null, - "rev": "e859e2f777521f82050b8f28e0205491a4ead0f5", + "rev": "96147eaa0c066a95210fe5518c987e77be034b9f", "opts": {}, "name": "«doc-gen4»", "inputRev?": "main", "inherited": false}}, - {"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "fb07d160aff0e8bdf403a78a5167fc7acf9c8227", - "opts": {}, - "name": "std", - "inputRev?": "main", - "inherited": true}}, {"git": {"url": "https://github.com/leanprover-community/quote4", "subDir?": null, - "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39", + "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755", "opts": {}, "name": "Qq", "inputRev?": "master", @@ -36,7 +28,7 @@ {"git": {"url": "https://github.com/leanprover-community/aesop", "subDir?": null, - "rev": "cb87803274405db79ec578fc07c4730c093efb90", + "rev": "bf5ab42a58e71de7ebad399ce3f90d29aae7fca9", "opts": {}, "name": "aesop", "inputRev?": "master", @@ -52,10 +44,18 @@ {"git": {"url": "https://github.com/leanprover-community/ProofWidgets4", "subDir?": null, - "rev": "f1a5c7808b001305ba07d8626f45ee054282f589", + "rev": "c3b9f0d4ebedc43635d3f7e764e277b1010844b7", "opts": {}, "name": "proofwidgets", - "inputRev?": "v0.0.21", + "inputRev?": "v0.0.22", + "inherited": true}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "c14f6a65b2c08caa38e1ab5db83451460d6cde3e", + "opts": {}, + "name": "std", + "inputRev?": "main", "inherited": true}}, {"git": {"url": "https://github.com/xubaiw/CMark.lean", diff --git a/lean-toolchain b/lean-toolchain index 734efddd..e8560170 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.3.0-rc1 \ No newline at end of file +leanprover/lean4:v4.3.0-rc1