bump

FltRegular/NumberTheory/AuxLemmas.lean

@@ -253,112 +253,6 @@ theorem Module.Finite.of_fintype_basis {R M} [CommSemiring R] [AddCommMonoid M]
     convert h.span_eq
     simp⟩⟩
 
--- Mathlib/RingTheory/Trace.lean
-lemma Algebra.trace_eq_of_algEquiv {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
-    [Algebra A B] [Algebra A C] (e : B ≃ₐ[A] C) (x) :
-    Algebra.trace A C (e x) = Algebra.trace A B x := by
-  by_cases hB : ∃ s : Finset B, Nonempty (Basis s A B)
-  · obtain ⟨s, ⟨b⟩⟩ := hB
-    haveI := Module.Finite.of_fintype_basis b
-    haveI := (Module.free_def A B).mpr ⟨_, ⟨b⟩⟩
-    haveI := Module.Finite.of_fintype_basis (b.map e.toLinearEquiv)
-    haveI := (Module.free_def A C).mpr ⟨_, ⟨(b.map e.toLinearEquiv).reindex (e.image _)⟩⟩
-    dsimp [Algebra.trace_apply]
-    rw [← LinearMap.trace_conj' _ e.toLinearEquiv]
-    congr
-    ext; simp [LinearEquiv.conj_apply]
-  rw [trace_eq_zero_of_not_exists_basis _ hB, trace_eq_zero_of_not_exists_basis]
-  rfl
-  intro ⟨s, ⟨b⟩⟩
-  classical
-  exact hB ⟨s.image e.symm, ⟨(b.map e.symm.toLinearEquiv).reindex
-    ((e.symm.image s).trans (Equiv.Set.ofEq Finset.coe_image.symm))⟩⟩
-
--- Mathlib/RingTheory/Trace.lean
-lemma Algebra.trace_eq_of_ringEquiv {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
-    [Algebra A C] [Algebra B C] (e : A ≃+* B) (he : (algebraMap B C).comp e = algebraMap A C) (x) :
-    e (Algebra.trace A C x) = Algebra.trace B C x := by
-  classical
-  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
-  · obtain ⟨s, ⟨b⟩⟩ := h
-    letI : Algebra A B := RingHom.toAlgebra e
-    letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
-    rw [Algebra.trace_eq_matrix_trace b,
-      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
-    show e.toAddMonoidHom _ = _
-    rw [AddMonoidHom.map_trace]
-    congr
-    ext i j
-    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
-  rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
-    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]
-  intro ⟨s, ⟨b⟩⟩
-  exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩
-
--- Mathlib/RingTheory/Trace.lean
-lemma Algebra.trace_eq_of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommRing A₁] [CommRing B₁]
-    [CommRing A₂] [CommRing B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂)
-    (he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁)) (x) :
-    Algebra.trace A₁ B₁ x = e₁.symm (Algebra.trace A₂ B₂ (e₂ x)) := by
-  letI := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra
-  let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl }
-  rw [← Algebra.trace_eq_of_ringEquiv e₁ he, ← Algebra.trace_eq_of_algEquiv e',
-    RingEquiv.symm_apply_apply]
-  rfl
-
--- Mathlib/RingTheory/Norm.lean
-lemma Algebra.norm_eq_of_algEquiv {A : Type u} {B : Type v} {C : Type w}
-    [CommRing A] [CommRing B] [CommRing C]
-    [Algebra A B] [Algebra A C] (e : B ≃ₐ[A] C) (x) :
-    Algebra.norm A (e x) = Algebra.norm A x := by
-  by_cases hB : ∃ s : Finset B, Nonempty (Basis s A B)
-  · obtain ⟨s, ⟨b⟩⟩ := hB
-    haveI := Module.Finite.of_fintype_basis b
-    haveI := (Module.free_def.{u, v, v} A B).mpr ⟨_, ⟨b⟩⟩
-    haveI := Module.Finite.of_fintype_basis (b.map e.toLinearEquiv)
-    haveI := (Module.free_def.{u, w, w} A C).mpr ⟨_, ⟨(b.map e.toLinearEquiv).reindex (e.image _)⟩⟩
-    dsimp [Algebra.norm_apply]
-    rw [← LinearMap.det_conj _ e.toLinearEquiv]
-    congr
-    ext; simp [LinearEquiv.conj_apply]
-  rw [norm_eq_one_of_not_exists_basis _ hB, norm_eq_one_of_not_exists_basis]
-  intro ⟨s, ⟨b⟩⟩
-  classical
-  exact hB ⟨s.image e.symm, ⟨(b.map e.symm.toLinearEquiv).reindex
-    ((e.symm.image s).trans (Equiv.Set.ofEq Finset.coe_image.symm))⟩⟩
-
--- Mathlib/RingTheory/Norm.lean
-lemma Algebra.norm_eq_of_ringEquiv {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
-    [Algebra A C] [Algebra B C] (e : A ≃+* B) (he : (algebraMap B C).comp e = algebraMap A C)
-    (x : C) :
-    e (Algebra.norm A x) = Algebra.norm B x := by
-  classical
-  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
-  · obtain ⟨s, ⟨b⟩⟩ := h
-    letI : Algebra A B := RingHom.toAlgebra e
-    letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
-    rw [Algebra.norm_eq_matrix_det b,
-      Algebra.norm_eq_matrix_det (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
-    show e.toRingHom _ = _
-    rw [RingHom.map_det]
-    congr
-    ext i j
-    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
-  rw [norm_eq_one_of_not_exists_basis _ h, norm_eq_one_of_not_exists_basis, map_one]
-  intro ⟨s, ⟨b⟩⟩
-  exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩
-
--- Mathlib/RingTheory/Norm.lean
-lemma Algebra.norm_eq_of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommRing A₁] [CommRing B₁]
-    [CommRing A₂] [CommRing B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂)
-    (he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁)) (x) :
-    Algebra.norm A₁ x = e₁.symm (Algebra.norm A₂ (e₂ x)) := by
-  letI := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra
-  let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl }
-  rw [← Algebra.norm_eq_of_ringEquiv e₁ he, ← Algebra.norm_eq_of_algEquiv e',
-    RingEquiv.symm_apply_apply]
-  rfl
-
 -- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
 lemma Matrix.mulVec_bijective {n R} [CommRing R] [Fintype n] [DecidableEq n]
     (M : Matrix n n R) (hM : IsUnit M.det) : Function.Bijective (mulVec M) := by

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "604b4078d46104d4144a87ebf4c2dae581cb704a",
+   "rev": "483fd2846f9fe5107011ece0cc3d8d88af1a8603",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "1ec84029c0ae659fd6e0cb972c81b327411ffd58",
+   "rev": "d85330ef0bdda6650271c95df08b6bd72a5a6459",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,