discr_powerBasis_eq_prod' — Mathlib

English

A variation of the power-basis discriminant formula: the same discriminant equals a product over i and j>i of the expression −((e_j g − e_i g)(e_i g − e_j g)).

Русский

Вариант формулы дискриминанта по базе степени: дискриминант равен произведению по парам i<j от выражения −((e_j(g) − e_i(g))(e_i(g) − e_j(g))).

LaTeX

$$$$ \\mathrm{algebraMap}_K^E(\\mathrm{discr}\\,K\\,pb.basis) = \\prod_{i

Lean4

/-- A variation of `Algebra.discr_powerBasis_eq_prod`. -/
theorem discr_powerBasis_eq_prod' [Algebra.IsSeparable K L] (e : Fin pb.dim ≃ (L →ₐ[K] E)) :
    algebraMap K E (discr K pb.basis) =
      ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, -((e j pb.gen - e i pb.gen) * (e i pb.gen - e j pb.gen)) :=
  by
  rw [discr_powerBasis_eq_prod _ _ _ e]
  congr; ext i; congr; ext j
  ring

Похожие утверждения