disc_of_degree_eq_one — Mathlib

English

The discriminant of a linear polynomial is 1.

Русский

Дискриминант линейного полинома равен 1.

LaTeX

$$$\\operatorname{disc} f = 1$ when $\\deg f = 1$$$

Lean4

/-- The discriminant of a linear polynomial is `1`. -/
theorem disc_of_degree_eq_one {f : R[X]} (hf : f.degree = 1) : disc f = 1 :=
  by
  rw [← Nat.cast_one, degree_eq_iff_natDegree_eq_of_pos one_pos] at hf
  let e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr (by cutsat)
  have : f.sylvesterDeriv.reindex e e = !![1] :=
    by
    have : NeZero (f.natDegree - 1 + f.natDegree) := ⟨by cutsat⟩
    ext ⟨i, hi⟩ ⟨j, hj⟩
    obtain ⟨rfl⟩ : i = 0 := by cutsat
    obtain ⟨rfl⟩ : j = 0 := by cutsat
    simp [e, sylvesterDeriv, mul_comm, hf]
  simp [disc, ← Matrix.det_reindex_self e, this, hf]

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