chore: golf and generalize discr_eq_discr_of_algEquiv (#9068)

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/NumberTheory/NumberField/Discriminant.lean

@@ -53,10 +53,7 @@ theorem discr_eq_discr {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι
 theorem discr_eq_discr_of_algEquiv {L : Type*} [Field L] [NumberField L] (f : K ≃ₐ[ℚ] L) :
     discr K = discr L := by
   let f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (f.restrictScalars ℤ).mapIntegralClosure.toLinearEquiv
-  let e : Module.Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →ₐ[ℚ] ℂ) := by
-    refine Fintype.equivOfCardEq ?_
-    rw [← FiniteDimensional.finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, AlgHom.card]
-  rw [← Rat.intCast_inj, coe_discr, Algebra.discr_eq_discr_of_algEquiv ℚ ℂ (integralBasis K) e f,
+  rw [← Rat.intCast_inj, coe_discr, Algebra.discr_eq_discr_of_algEquiv (integralBasis K) f,
     ← discr_eq_discr L ((RingOfIntegers.basis K).map f₀)]
   change _ = algebraMap ℤ ℚ _
   rw [← Algebra.discr_localizationLocalization ℤ (nonZeroDivisors ℤ) L]

Mathlib/RingTheory/Discriminant.lean

@@ -75,6 +75,12 @@ theorem discr_def [Fintype ι] (b : ι → B) : discr A b = (traceMatrix A b).de
   unfold discr
   convert rfl
 
+variable {A C} in
+/-- Mapping a family of vectors along an `AlgEquiv` preserves the discriminant. -/
+theorem discr_eq_discr_of_algEquiv [Fintype ι] (b : ι → B) (f : B ≃ₐ[A] C) :
+    Algebra.discr A b = Algebra.discr A (f ∘ b) := by
+  rw [discr_def]; congr; ext
+  simp_rw [traceMatrix_apply, traceForm_apply, Function.comp, ← map_mul f, trace_eq_of_algEquiv]
 
 #align algebra.discr_def Algebra.discr_def
 
@@ -132,7 +138,7 @@ variable [Algebra K L] [Algebra K E]
 
 variable [Module.Finite K L] [IsAlgClosed E]
 
-/-- Over a field, if `b` is a basis, then `Algebra.discr K b ≠ 0`. -/
+/-- If `b` is a basis of a finite separable field extension `L/K`, then `Algebra.discr K b ≠ 0`. -/
 theorem discr_not_zero_of_basis [IsSeparable K L] (b : Basis ι K L) :
     discr K b ≠ 0 := by
   cases isEmpty_or_nonempty ι
@@ -150,7 +156,8 @@ theorem discr_not_zero_of_basis [IsSeparable K L] (b : Basis ι K L) :
     exact traceForm_nondegenerate _ _
 #align algebra.discr_not_zero_of_basis Algebra.discr_not_zero_of_basis
 
-/-- Over a field, if `b` is a basis, then `Algebra.discr K b` is a unit. -/
+/-- If `b` is a basis of a finite separable field extension `L/K`,
+  then `Algebra.discr K b` is a unit. -/
 theorem discr_isUnit_of_basis [IsSeparable K L] (b : Basis ι K L) : IsUnit (discr K b) :=
   IsUnit.mk0 _ (discr_not_zero_of_basis _ _)
 #align algebra.discr_is_unit_of_basis Algebra.discr_isUnit_of_basis
@@ -167,20 +174,6 @@ theorem discr_eq_det_embeddingsMatrixReindex_pow_two [IsSeparable K L] (e : ι 
     traceMatrix_eq_embeddingsMatrixReindex_mul_trans, det_mul, det_transpose, pow_two]
 #align algebra.discr_eq_det_embeddings_matrix_reindex_pow_two Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two
 
-/-- Mapping a family of vectors along an `AlgEquiv` preserves the discriminant. -/
-theorem discr_eq_discr_of_algEquiv {L' : Type*} [Field L'] [Algebra K L'] [IsSeparable K L]
-    (e : ι ≃ (L →ₐ[K] E)) (f : L ≃ₐ[K] L') :
-    Algebra.discr K b = Algebra.discr K (f ∘ b) := by
-  have : Module.Finite K L' := Module.Finite.equiv f.toLinearEquiv
-  have : IsSeparable K L' := IsSeparable.of_algHom K L f.symm
-  apply (NoZeroSMulDivisors.algebraMap_injective K E)
-  let e' : ι ≃ (L' →ₐ[K] E) := e.trans (f.arrowCongr AlgEquiv.refl)
-  rw [Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two _ _ _ e,
-    Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two _ _ _ e']
-  congr
-  ext
-  simp [Algebra.embeddingsMatrixReindex]
-
 /-- The discriminant of a power basis. -/
 theorem discr_powerBasis_eq_prod (e : Fin pb.dim ≃ (L →ₐ[K] E)) [IsSeparable K L] :
     algebraMap K E (discr K pb.basis) =