English
Let L/K be a finite separable extension with a power basis pb. For an equivalence e : Fin pb.dim ≃ (L →ₐ[K] E), the discriminant of the power basis equals the Vandermonde-like product on the conjugates: algebraMap_K_E(discr_K(pb.basis)) = ∏_{i<j} (e_j(pb.gen) − e_i(pb.gen))^2.
Русский
Пусть L/K — конечное разделимое расширение; pb — база в виде степени, имеющая генераторы pb.gen. При биекции e между индексами и алгебраическими вложениями L → E дискриминант базы равен произведению по парам индексов i<j от квадрата разности значений: algebraMap_K_E(discr_K(pb.basis)) = ∏_{i<j} (e_j(pb.gen) − e_i(pb.gen))^2.
LaTeX
$$$$ algebraMap_K_E(\\mathrm{discr}\\,K\\,pb.basis) = \\prod_{i : Fin\\ pb.dim} \\prod_{j \\in Ioi i} (e\\,j\\,pb.gen - e\\,i\\,pb.gen)^2 $$$$
Lean4
/-- The discriminant of a power basis. -/
theorem discr_powerBasis_eq_prod (e : Fin pb.dim ≃ (L →ₐ[K] E)) [Algebra.IsSeparable K L] :
algebraMap K E (discr K pb.basis) = ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, (e j pb.gen - e i pb.gen) ^ 2 :=
by
rw [discr_eq_det_embeddingsMatrixReindex_pow_two K E pb.basis e, embeddingsMatrixReindex_eq_vandermonde,
det_transpose, det_vandermonde, ← prod_pow]
congr; ext i
rw [← prod_pow]
