bump

FltRegular/NumberTheory/AuxLemmas.lean

@@ -264,22 +264,6 @@ lemma Matrix.mulVec_injective {n R} [CommRing R] [Fintype n] [DecidableEq n]
     (M : Matrix n n R) (hM : IsUnit M.det) : Function.Injective (mulVec M) :=
   (M.mulVec_bijective hM).injective
 
--- Mathlib/RingTheory/FractionalIdeal.lean
-namespace FractionalIdeal
-
-open nonZeroDivisors
-
-variable {R K} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDedekindDomain R]
-variable {I J : FractionalIdeal R⁰ K}
-
-lemma le_inv_comm (hI : I ≠ 0) (hJ : J ≠ 0) : I ≤ J⁻¹ ↔ J ≤ I⁻¹ := by
-  rw [inv_eq_one_div, inv_eq_one_div, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]
-
-lemma inv_le_comm (hI : I ≠ 0) (hJ : J ≠ 0) : I⁻¹ ≤ J ↔ J⁻¹ ≤ I := by
-  simpa using le_inv_comm (inv_ne_zero hI) (inv_ne_zero hJ)
-
-end FractionalIdeal
-
 -- -- Mathlib/RingTheory/Localization/FractionRing.lean
 -- noncomputable
 -- instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B]

FltRegular/NumberTheory/Different.lean

@@ -189,89 +189,9 @@ lemma FractionalIdeal.le_dual₂_inv_aux (I J: FractionalIdeal B⁰ L) (hI) (hIJ
 variable [IsDedekindDomain B] [IsFractionRing B L]
 
 variable (A K)
-
-lemma FractionalIdeal.inv_le_dual₂ (I : FractionalIdeal B⁰ L) (hI) :
-    I⁻¹ ≤ dual₂ A K I hI :=
-  le_dual₂_inv_aux _ _ _ (le_of_eq (mul_inv_cancel hI))
-
-lemma FractionalIdeal.dual₂_inv_le (I : FractionalIdeal B⁰ L) (hI) :
-    (dual₂ A K I hI)⁻¹ ≤ I := by
-  convert mul_right_mono ((dual₂ A K I hI)⁻¹)
-    (mul_left_mono I (FractionalIdeal.inv_le_dual₂ A K I hI)) using 1
-  · simp only [mul_inv_cancel hI, one_mul]
-  · simp only [mul_inv_cancel (FractionalIdeal.dual₂_ne_zero (hI := hI)), mul_assoc, mul_one]
-
 variable (B)
-
-def differentIdeal [NoZeroSMulDivisors A B] : Ideal B :=
-  (1 / traceFormDualSubmodule A (FractionRing A) 1 : Submodule B (FractionRing B)).comap
-    (Algebra.linearMap B (FractionRing B))
-
-lemma coeSubmodule_differentIdeal' [NoZeroSMulDivisors A B] (hAB : Algebra.IsIntegral A B)
-    [IsSeparable (FractionRing A) (FractionRing B)]
-    [FiniteDimensional (FractionRing A) (FractionRing B)] :
-    coeSubmodule (FractionRing B) (differentIdeal A B) =
-      1 / traceFormDualSubmodule A (FractionRing A) 1 := by
-  have : IsIntegralClosure B A (FractionRing B) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ hAB
-  rw [coeSubmodule, differentIdeal, Submodule.map_comap_eq, inf_eq_right]
-  have := FractionalIdeal.dual₂_inv_le A (FractionRing A) (1 : FractionalIdeal B⁰ (FractionRing B))
-    one_ne_zero
-  have : _ ≤ ((1 : FractionalIdeal B⁰ (FractionRing B)) : Submodule B (FractionRing B)) := this
-  simp only [← one_div, FractionalIdeal.val_eq_coe,
-    FractionalIdeal.coe_div FractionalIdeal.dual₂_ne_zero] at this
-  dsimp [FractionalIdeal.dual₂] at this
-  simpa only [FractionalIdeal.coe_one] using this
-
-lemma coeSubmodule_differentIdeal [NoZeroSMulDivisors A B] :
-    coeSubmodule L (differentIdeal A B) = 1 / traceFormDualSubmodule A K 1 := by
-  have : (FractionRing.algEquiv B L).toLinearEquiv.comp (Algebra.linearMap B (FractionRing B)) =
-    Algebra.linearMap B L := by ext; simp
-  rw [coeSubmodule, ← this]
-  have H : RingHom.comp (algebraMap (FractionRing A) (FractionRing B))
-    ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
-      RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L)
-  · apply IsLocalization.ringHom_ext A⁰
-    ext
-    simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
-      AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
-      ← IsScalarTower.algebraMap_apply]
-    rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
-  have : IsSeparable (FractionRing A) (FractionRing B) := IsSeparable_of_equiv_equiv _ _ H
-  have : FiniteDimensional (FractionRing A) (FractionRing B) := Module.Finite_of_equiv_equiv _ _ H
-  simp only [AlgEquiv.toLinearEquiv_toLinearMap, Submodule.map_comp]
-  rw [← coeSubmodule, coeSubmodule_differentIdeal' _ _ (IsIntegralClosure.isIntegral_algebra _ L),
-    Submodule.map_div, ← AlgEquiv.toAlgHom_toLinearMap, Submodule.map_one]
-  congr 1
-  refine (map_equiv_traceFormDualSubmodule A K _).trans ?_
-  congr 1
-  ext
-  simp
-
 variable (L)
 
-lemma coeIdeal_different_ideal [NoZeroSMulDivisors A B] :
-    ↑(differentIdeal A B) =
-      (FractionalIdeal.dual₂ A K (1 : FractionalIdeal B⁰ L) one_ne_zero)⁻¹ := by
-  apply FractionalIdeal.coeToSubmodule_injective
-  simp only [FractionalIdeal.coe_div FractionalIdeal.dual₂_ne_zero,
-    FractionalIdeal.coe_coeIdeal, coeSubmodule_differentIdeal A K, inv_eq_one_div]
-  simp only [FractionalIdeal.dual₂, FractionalIdeal.coe_mk, FractionalIdeal.coe_one]
-
-lemma differentialIdeal_le_fractionalIdeal_iff
-  (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) [NoZeroSMulDivisors A B] :
-    differentIdeal A B ≤ I ↔ (((I⁻¹ : _) : Submodule B L).restrictScalars A).map
-      ((Algebra.trace K L).restrictScalars A) ≤ 1 := by
-  rw [coeIdeal_different_ideal A K B L, FractionalIdeal.inv_le_comm FractionalIdeal.dual₂_ne_zero hI]
-  refine le_traceFormDualSubmodule.trans ?_
-  simp
-
-lemma differentialIdeal_le_iff (I : Ideal B) (hI : I ≠ ⊥) [NoZeroSMulDivisors A B] :
-    differentIdeal A B ≤ I ↔ (((I⁻¹ : FractionalIdeal B⁰ L) : Submodule B L).restrictScalars A).map
-      ((Algebra.trace K L).restrictScalars A) ≤ 1 :=
-  (FractionalIdeal.coeIdeal_le_coeIdeal _).symm.trans
-    (differentialIdeal_le_fractionalIdeal_iff A K B L (I : FractionalIdeal B⁰ L) (by simpa))
-
 lemma pow_sub_one_dvd_differentIdeal_aux
     [IsDedekindDomain A] [NoZeroSMulDivisors A B] [Module.Finite A B]
     {p : Ideal A} [p.IsMaximal] (P : Ideal B) (e : ℕ) (he : 0 < e) (hp : p ≠ ⊥)
@@ -297,7 +217,7 @@ lemma pow_sub_one_dvd_differentIdeal_aux
       simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div, ne_eq,
         FractionalIdeal.coeIdeal_eq_zero, mul_div_assoc]
       rw [div_self (by simpa), mul_one]
-    rw [Ideal.dvd_iff_le, differentialIdeal_le_iff A K B L _ (pow_ne_zero _ hPbot), hP,
+    rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) (pow_ne_zero _ hPbot), hP,
       Submodule.map_le_iff_le_comap]
     intro x hx
     rw [Submodule.restrictScalars_mem, FractionalIdeal.mem_coe,
@@ -411,12 +331,13 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
     (x : B) (hx : Algebra.adjoin K {algebraMap B L x} = ⊤) :
     (conductor A x) * differentIdeal A B = Ideal.span {aeval x (derivative (minpoly A x))} := by
   classical
+  have onz := one_ne_zero (α := FractionalIdeal B⁰ L)
   have hAx : IsIntegral A x := IsIntegralClosure.isIntegral A L x
   haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
   apply FractionalIdeal.coeIdeal_injective (K := L)
   simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton]
-  rw [coeIdeal_different_ideal A K B L,
-    mul_inv_eq_iff_eq_mul₀ FractionalIdeal.dual₂_ne_zero]
+  rw [coeIdeal_differentIdeal A K L B,
+    mul_inv_eq_iff_eq_mul₀ (FractionalIdeal.dual_ne_zero A K onz)]
   apply FractionalIdeal.coeToSubmodule_injective
   simp only [FractionalIdeal.coe_coeIdeal, FractionalIdeal.coe_mul,
     FractionalIdeal.coe_spanSingleton, Submodule.span_singleton_mul]
@@ -426,7 +347,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
   have : algebraMap B L (aeval x (derivative (minpoly A x))) ≠ 0
   · rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
       aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁
-  rw [Submodule.mem_smul_iff_inv this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual₂,
+  rw [Submodule.mem_smul_iff_inv this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual onz,
     mem_coeIdeal_conductor]
   have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0
   · rwa [ne_eq, inv_eq_zero]

FltRegular/NumberTheory/Finrank.lean

@@ -160,8 +160,9 @@ lemma Module.finite_iff_rank_lt_aleph0 [Module R M] [Module.Free R M] :
       Set.finite_coe_iff.mpr ((Module.Free.chooseBasis R M).finite_index_of_rank_lt_aleph0 H)
     exact Module.Finite.of_basis (Module.Free.chooseBasis R M)
 
-lemma Module.finite_of_finrank_pos [Module.Free R M] (hf : 0 < FiniteDimensional.finrank R M) :
-    Module.Finite R M := Module.finite_iff_rank_lt_aleph0.mpr (Cardinal.toNat_pos.mp hf).2
+@[deprecated Module.finite_of_finrank_pos]
+lemma Module.finite_of_finrank_pos' [Module.Free R M] (hf : 0 < FiniteDimensional.finrank R M) :
+    Module.Finite R M := finite_of_finrank_pos hf
 
 lemma FiniteDimensional.finrank_quotient_of_le_torsion (hN : N ≤ Submodule.torsion R M) :
     finrank R (M ⧸ N) = finrank R M := by
@@ -211,21 +212,10 @@ lemma FiniteDimensional.finrank_of_surjective_of_le_torsion {M'} [AddCommGroup M
   rw [← LinearMap.range_eq_map l, LinearMap.range_eq_top.mpr hl] at this
   simpa only [finrank_top] using this
 
-lemma FiniteDimensional.finrank_eq_zero_iff [IsDomain R] :
-    finrank R M = 0 ↔ Module.IsTorsion R M := by
-  constructor
-  · delta Module.IsTorsion
-    contrapose!
-    rintro ⟨x, hx⟩
-    rw [← Nat.one_le_iff_ne_zero]
-    have : LinearIndependent R (fun _ : Unit ↦ x)
-    · exact linearIndependent_iff.mpr (fun l hl ↦ Finsupp.unique_ext <| not_not.mp fun H ↦
-        hx ⟨_, mem_nonZeroDivisors_of_ne_zero H⟩ ((Finsupp.total_unique _ _ _).symm.trans hl))
-    exact FiniteDimensional.fintype_card_le_finrank_of_linearIndependent' this
-  · intro h
-    rw [← FiniteDimensional.finrank_quotient_of_le_torsion _
-      ((Submodule.isTorsion'_iff_torsion'_eq_top (R := R) _).mp h).ge]
-    exact finrank_zero_of_subsingleton
+@[deprecated FiniteDimensional.finrank_eq_zero_iff_isTorsion]
+lemma FiniteDimensional.finrank_eq_zero_iff' [IsDomain R] :
+    finrank R M = 0 ↔ Module.IsTorsion R M :=
+  FiniteDimensional.finrank_eq_zero_iff_isTorsion
 
 lemma FiniteDimensional.finrank_add_finrank_quotient_of_free [IsDomain R] [IsPrincipalIdealRing R]
     [Module.Free R M]

FltRegular/NumberTheory/GaloisPrime.lean

@@ -1,4 +1,5 @@
 import FltRegular.NumberTheory.AuxLemmas
+import Mathlib.RingTheory.IntegralRestrict
 
 /-!
 # Galois action on primes
@@ -110,54 +111,20 @@ variable (R K S L : Type*) [CommRing R] [CommRing S] [Algebra R S] [Field K] [Fi
     [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] -- [IsNoetherian R S]
     [IsIntegralClosure S R L] [FiniteDimensional K L]
 
-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 ↦ IsIntegral.map _ (IsIntegralClosure.isIntegral R L x)))
-  map_one' := by
-    ext x
-    apply (IsIntegralClosure.equiv R (integralClosure R L) L S).symm.injective
-    ext
-    dsimp
-    simp only [AlgEquiv.symm_apply_apply, AlgHom.coe_codRestrict, AlgHom.coe_comp,
-      AlgHom.coe_restrictScalars', IsScalarTower.coe_toAlgHom', Function.comp_apply,
-      AlgHom.one_apply]
-    exact (IsIntegralClosure.algebraMap_equiv R S L (integralClosure R L) x).symm
-  map_mul' := by
-    intros σ₁ σ₂
-    ext x
-    apply (IsIntegralClosure.equiv R (integralClosure R L) L S).symm.injective
-    ext
-    dsimp
-    simp only [AlgEquiv.symm_apply_apply, AlgHom.coe_codRestrict, AlgHom.coe_comp,
-      AlgHom.coe_restrictScalars', IsScalarTower.coe_toAlgHom', Function.comp_apply,
-      AlgHom.mul_apply, IsIntegralClosure.algebraMap_equiv, Subalgebra.algebraMap_eq]
-    dsimp
-
-lemma algebraMap_galRestrictHom_apply (σ : L →ₐ[K] L) (x : S) :
-    algebraMap S L (galRestrictHom R K S L σ x) = σ (algebraMap S L x) := by
-  simp [galRestrictHom, Subalgebra.algebraMap_eq]
-
 lemma prod_galRestrictHom_eq_norm [IsGalois K L] (x) :
-    (∏ σ : L ≃ₐ[K] L, galRestrictHom R K S L σ x) =
+    (∏ σ : L ≃ₐ[K] L, galRestrictHom R K L S σ x) =
     algebraMap R S (IsIntegralClosure.mk' (R := R) R (Algebra.norm K <| algebraMap S L x)
       (Algebra.isIntegral_norm K (IsIntegralClosure.isIntegral R L x).algebraMap)) := by
   apply IsIntegralClosure.algebraMap_injective S R L
   rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_eq R K L]
   simp only [map_prod, algebraMap_galRestrictHom_apply, IsIntegralClosure.algebraMap_mk',
     Algebra.norm_eq_prod_automorphisms, AlgHom.coe_coe, RingHom.coe_comp, Function.comp_apply]
 
-noncomputable
-def galRestrict : (L ≃ₐ[K] L) →* (S ≃ₐ[R] S) :=
-  MonoidHom.comp (algHomUnitsEquiv R S)
-    ((Units.map <| galRestrictHom R K S L).comp (algHomUnitsEquiv K L).symm)
-
 noncomputable
 instance (p : Ideal R) : MulAction (L ≃ₐ[K] L) (primesOver S p) where
-  smul := fun σ P ↦ ⟨Ideal.comap (galRestrict R K S L σ⁻¹) P, P.2.1.comap _, by
+  smul := fun σ P ↦ ⟨Ideal.comap (galRestrict R K L S σ⁻¹) P, P.2.1.comap _, by
     refine Eq.trans ?_ P.2.2
-    rw [← Ideal.comap_coe (galRestrict R K S L _), Ideal.comap_comap,
+    rw [← Ideal.comap_coe (galRestrict R K L S _), Ideal.comap_comap,
       ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]⟩
   one_smul := by
     intro p
@@ -169,12 +136,12 @@ instance (p : Ideal R) : MulAction (L ≃ₐ[K] L) (primesOver S p) where
     intro σ₁ σ₂ p
     ext1
     show Ideal.comap _ _ = Ideal.comap _ (Ideal.comap _ _)
-    rw [← Ideal.comap_coe (galRestrict R K S L _), ← Ideal.comap_coe (galRestrict R K S L _),
-      ← Ideal.comap_coe (galRestrict R K S L _), Ideal.comap_comap, mul_inv_rev, map_mul]
+    rw [← Ideal.comap_coe (galRestrict R K L S _), ← Ideal.comap_coe (galRestrict R K L S _),
+      ← Ideal.comap_coe (galRestrict R K L S _), Ideal.comap_comap, mul_inv_rev, map_mul]
     rfl
 
 lemma coe_smul_primesOver {p : Ideal R} (σ : L ≃ₐ[K] L) (P : primesOver S p) :
-  (↑(σ • P) : Ideal S) = Ideal.comap (galRestrict R K S L σ⁻¹) P := rfl
+  (↑(σ • P) : Ideal S) = Ideal.comap (galRestrict R K L S σ⁻¹) P := rfl
 
 open BigOperators
 
@@ -221,15 +188,15 @@ instance [IsGalois K L] (p : Ideal R) :
   have hQ := Q.prop.1
   -- Then `σ y ∉ Q` for all `σ`, or else `1 = x + y ∈ σ⁻¹ • Q`.
   -- This implies that `∏ σ y ∉ Q`.
-  have : ∏ σ : L ≃ₐ[K] L, galRestrictHom R K S L σ y ∉ (Q : Ideal S)
+  have : ∏ σ : L ≃ₐ[K] L, galRestrictHom R K L S σ y ∉ (Q : Ideal S)
   · apply prod_mem (S := (Q : Ideal S).primeCompl)
     intro σ _ hσ
     apply (isMaximal_of_mem_primesOver hp (σ⁻¹ • Q).prop).ne_top
     rw [Ideal.eq_top_iff_one, ← hxy]
     apply add_mem
     · suffices ↑(σ⁻¹ • Q) ∣ I from (Ideal.dvd_iff_le.mp this) hx
       exact Finset.dvd_prod_of_mem _ (Finset.mem_univ _)
-    · show galRestrictHom R K S L ↑(σ⁻¹⁻¹) y ∈ (Q : Ideal S)
+    · show galRestrictHom R K L S ↑(σ⁻¹⁻¹) y ∈ (Q : Ideal S)
       rwa [inv_inv]
   -- OTOH we show that `∏ σ y ∈ Q`.
   -- Since `∏ σ y` is the norm of `y ∈ P`, it falls in `R ∩ Q = p = R ∩ P` as desired.
@@ -240,14 +207,14 @@ instance [IsGalois K L] (p : Ideal R) :
   apply hy
   rw [Ideal.mem_span_singleton]
   refine dvd_trans ?_ (Finset.dvd_prod_of_mem _ (Finset.mem_univ 1))
-  show y ∣ galRestrictHom R K S L 1 y
+  show y ∣ galRestrictHom R K L S 1 y
   rw [map_one]
   exact dvd_rfl
   -- Which gives a contradiction and hence there is some `σ` such that `σ • P = Q`.
 
 lemma exists_comap_galRestrict_eq [IsGalois K L] {p : Ideal R} {P₁ P₂ : Ideal S}
     (hP₁ : P₁ ∈ primesOver S p) (hP₂ : P₂ ∈ primesOver S p) :
-    ∃ σ, P₁.comap (galRestrict R K S L σ) = P₂ :=
+    ∃ σ, P₁.comap (galRestrict R K L S σ) = P₂ :=
 ⟨_, congr_arg Subtype.val (MulAction.exists_smul_eq (L ≃ₐ[K] L)
   (⟨P₁, hP₁⟩ : primesOver S p) ⟨P₂, hP₂⟩).choose_spec⟩
 
@@ -298,7 +265,7 @@ lemma Ideal.ramificationIdxIn_eq_ramificationIdx [IsGalois K L] (p : Ideal R) (P
   rw [dif_pos this]
   have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K S L hP this.choose_spec
   rw [← hσ]
-  exact Ideal.ramificationIdx_comap_eq (galRestrict R K S L σ) p P
+  exact Ideal.ramificationIdx_comap_eq (galRestrict R K L S σ) p P
 
 lemma Ideal.inertiaDegIn_eq_inertiaDeg [IsGalois K L] (p : Ideal R) (P : Ideal S)
     (hP : P ∈ primesOver S p) [p.IsMaximal] :
@@ -308,7 +275,7 @@ lemma Ideal.inertiaDegIn_eq_inertiaDeg [IsGalois K L] (p : Ideal R) (P : Ideal S
   rw [dif_pos this]
   have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K S L hP this.choose_spec
   rw [← hσ]
-  exact Ideal.inertiaDeg_comap_eq (galRestrict R K S L σ) p P
+  exact Ideal.inertiaDeg_comap_eq (galRestrict R K L S σ) p P
 
 open FiniteDimensional
 
@@ -393,7 +360,7 @@ lemma prod_smul_primesOver [IsGalois K L] (p : Ideal R) (P : primesOver S p) [p.
     simp_rw [primesOver_bot (S := S) (IsIntegralClosure.isIntegral_algebra R L),
       Set.mem_singleton_iff] at this
     simp_rw [coe_smul_primesOver, this,
-      Ideal.comap_bot_of_injective _ (galRestrict R K S L _).injective, Finset.prod_const,
+      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]

FltRegular/NumberTheory/Hilbert90.lean

@@ -131,7 +131,7 @@ variable [IsIntegralClosure B A L] [IsDomain B]
 
 lemma Hilbert90_integral (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ)
     (η : B) (hη : Algebra.norm K (algebraMap B L η) = 1) :
-    ∃ ε : B, ε ≠ 0 ∧ η * galRestrict A K B L σ ε = ε := by
+    ∃ ε : B, ε ≠ 0 ∧ η * galRestrict A K L B σ ε = ε := by
   haveI : NoZeroSMulDivisors A L := by
     rw [NoZeroSMulDivisors.iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
     exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
@@ -157,7 +157,7 @@ lemma Hilbert90_integral (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowe
     apply IsIntegralClosure.algebraMap_injective B A L
     rw [map_mul, ← hε]
     congr 1
-    exact algebraMap_galRestrictHom_apply A K B L σ x
+    exact algebraMap_galRestrictHom_apply A K L B σ x
     · intro e
       rw [(map_eq_zero _).mp e, zero_div] at hε
       rw [hε, Algebra.norm_zero] at hη