discr_powerBasis_eq_prod'' — Mathlib

English

A refinement of the discriminant formula for a power basis, introducing a sign factor (−1)^{n(n−1)/2} times a symmetric product of differences between embeddings.

Русский

Уточнение формулы дискриминанта базы степени с дополнительным знаком (−1)^{n(n−1)/2} и симметричным произведением разностей значений вложений.

LaTeX

$$$$ \\mathrm{discr}_K(pb.basis) = (-1)^{\\frac{n(n-1)}{2}} \\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) =
      (-1) ^ (n * (n - 1) / 2) * ∏ 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]
  simp_rw [fun i j => neg_eq_neg_one_mul ((e j pb.gen - e i pb.gen) * (e i pb.gen - e j pb.gen)), prod_mul_distrib]
  congr
  simp only [prod_pow_eq_pow_sum, prod_const]
  congr
  rw [← @Nat.cast_inj ℚ, Nat.cast_sum]
  have : ∀ x : Fin pb.dim, ↑x + 1 ≤ pb.dim := by simp [Nat.succ_le_iff, Fin.is_lt]
  simp_rw [Fin.card_Ioi, Nat.sub_sub, add_comm 1]
  simp only [Nat.cast_sub, this, Finset.card_fin, nsmul_eq_mul, sum_const, sum_sub_distrib, Nat.cast_add, Nat.cast_one,
    sum_add_distrib, mul_one]
  rw [← Nat.cast_sum, ← @Finset.sum_range ℕ _ pb.dim fun i => i, sum_range_id]
  have hn : n = pb.dim :=
    by
    rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim]
      -- FIXME: Without the `Fintype` namespace, why does it complain about `Finset.card_congr` being
          -- deprecated?

    exact Fintype.card_congr e.symm
  have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := pb.dim.even_mul_pred_self.two_dvd
  have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp
  have hle : 1 ≤ pb.dim :=
    by
    rw [← hn, Nat.one_le_iff_ne_zero, ← zero_lt_iff, Module.finrank_pos_iff]
    infer_instance
  rw [hn, Nat.cast_div h₂ hne, Nat.cast_mul, Nat.cast_sub hle]
  field_simp
  ring

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