From 3a8e53dafa3fb71b6d643b74b0c331e711fe5b00 Mon Sep 17 00:00:00 2001 From: riccardobrasca Date: Mon, 27 Nov 2023 21:22:30 +0100 Subject: [PATCH] bump --- FltRegular/NumberTheory/AuxLemmas.lean | 25 +++++-------------------- FltRegular/NumberTheory/Hilbert90.lean | 3 +-- lake-manifest.json | 2 +- 3 files changed, 7 insertions(+), 23 deletions(-) diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index 00009d8c..530f7096 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/FltRegular/NumberTheory/AuxLemmas.lean @@ -164,10 +164,6 @@ lemma Ideal.inertiaDeg_comap_eq (e : S₁ ≃ₐ[R] S₂) (p : Ideal R) (P : Ide end RamificationInertia --- Mathlib/RingTheory/Nilpotent.lean -theorem not_isNilpotent_one {R : Type*} [MonoidWithZero R] [Nontrivial R] : - ¬ IsNilpotent (1 : R) := fun ⟨_, H⟩ ↦ zero_ne_one (H.symm.trans (one_pow _)) - open Polynomial IntermediateField -- Mathlib/FieldTheory/Adjoin.lean @@ -317,18 +313,6 @@ lemma Module.End.HasEigenvector.pow_apply {R} [CommRing R] {M} [AddCommGroup M] (hv : f.HasEigenvector μ v) (n : ℕ) : (f ^ n) v = μ ^ n • v := by induction n <;> simp [*, pow_succ f, hv.apply_eq_smul, smul_smul, pow_succ' μ] --- Mathlib/Algebra/Module/Submodule/Basic.lean -lemma Submodule.restrictScalars_mul {A B C} [CommSemiring A] [CommSemiring B] [Semiring C] - [Algebra A B] [Algebra A C] [Algebra B C] [IsScalarTower A B C] {I J : Submodule B C} : - (I * J).restrictScalars A = I.restrictScalars A * J.restrictScalars A := by - apply le_antisymm - · intro x (hx : x ∈ I * J) - refine Submodule.mul_induction_on hx ?_ ?_ - · exact fun m hm n hn ↦ Submodule.mul_mem_mul hm hn - · exact fun _ _ ↦ add_mem - · apply Submodule.mul_le.mpr - exact fun m hm n hn ↦ Submodule.mul_mem_mul hm hn - -- Mathlib/Logic/Equiv/Defs.lean lemma EquivLike.coe_coe {E α β : Sort*} [EquivLike E α β] (e : E) : ((e : α ≃ β) : α → β) = e := rfl @@ -1070,8 +1054,8 @@ lemma Matrix.eval_det_add_X_smul {n} [Fintype n] [DecidableEq n] {R} [CommRing R (A) (M : Matrix n n R) : (det (A + (X : R[X]) • M.map C)).eval 0 = (det A).eval 0 := by simp only [eval_det, map_zero, map_add, eval_add, Algebra.smul_def, _root_.map_mul] - simp only [algebraMap_eq_smul, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X, mul_zero, - add_zero] + simp only [Algebra.algebraMap_eq_smul_one, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X, + mul_zero, add_zero] -- Mathlib/LinearAlgebra/Matrix/Trace.lean lemma Matrix.trace_submatrix_succ {n : ℕ} {R} [CommRing R] (M : Matrix (Fin n.succ) (Fin n.succ) R) : @@ -1136,14 +1120,15 @@ lemma Matrix.det_one_add_smul {n} [Fintype n] [DecidableEq n] {R} [CommRing R] ( (M : Matrix n n R) : det (1 + r • M) = 1 + trace M * r + (det (1 + (X : R[X]) • M.map C)).divX.divX.eval r * r ^ 2 := by have := congr_arg (eval r) (Matrix.det_one_add_X_smul M) - simp only [eval_det, coe_scalar, map_add, _root_.map_one, eval_add, eval_one, eval_smul, eval_X, + simp only [eval_det, scalar_apply, map_add, _root_.map_one, eval_add, eval_one, eval_smul, eval_X, smul_eq_mul, eval_mul, eval_pow] at this convert this rw [Algebra.smul_def X, _root_.map_mul] have : matPolyEquiv (M.map C) = C M · ext; simp only [matPolyEquiv_coeff_apply, map_apply, coeff_C]; rw [ite_apply, ite_apply]; rfl - simp only [algebraMap_eq_smul, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X, this, + simp only [Algebra.algebraMap_eq_smul_one, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X, this, Algebra.mul_smul_comm, mul_one, eval_C] + exact Matrix.smul_eq_mul_diagonal _ _ lemma Algebra.norm_one_add_smul {A B} [CommRing A] [CommRing B] [Algebra A B] [Module.Free A B] [Module.Finite A B] (a : A) (x : B) : diff --git a/FltRegular/NumberTheory/Hilbert90.lean b/FltRegular/NumberTheory/Hilbert90.lean index 7d339f33..97927c85 100644 --- a/FltRegular/NumberTheory/Hilbert90.lean +++ b/FltRegular/NumberTheory/Hilbert90.lean @@ -26,8 +26,7 @@ def φ := (finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm variable {σ} lemma hφ : ∀ (n : ℕ), φ σ ⟨σ ^ n, hσ _⟩ = n % (orderOf σ) := fun n ↦ by - simpa [Fin.ext_iff] using - @finEquivZpowers_symm_apply _ _ _ (isOfFinOrder_of_finite σ) n ⟨n, by simp⟩ + simpa [Fin.ext_iff] using finEquivZpowers_symm_apply _ (isOfFinOrder_of_finite σ) n noncomputable def cocycle : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i in range (φ σ ⟨τ, hσ τ⟩), Units.map (σ ^ i) (ηu hη) diff --git a/lake-manifest.json b/lake-manifest.json index a79d5f7d..a41ecc3c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "83d4f222771f491b351d70b070406481f5d2b2ba", + "rev": "313ebb4380e5fca7f4cf6a610956a4b5a934235a", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,