univ_coeff_card — Mathlib

English

The coefficient of degree card(n) in the universal polynomial is 1.

Русский

Коэффициент при степени card(n) в универсальном полиноме равен 1.

LaTeX

$$$(\\mathrm{charpoly.univ}\\,R\\,n).\\operatorname{coeff}(\\operatorname{Fintype.card} n) = 1$$$

Lean4

@[simp]
theorem univ_coeff_card : (univ R n).coeff (Fintype.card n) = 1 :=
  by
  suffices Polynomial.coeff (univ ℤ n) (Fintype.card n) = 1 by
    rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, map_one]
  rw [← univ_natDegree ℤ n]
  exact (univ_monic ℤ n).leadingCoeff

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