univ_coeff_isHomogeneous — Mathlib

English

For i, j with i + j = card n, the i-th coefficient of the universal polynomial is homogeneous of degree j.

Русский

Для i, j с i+j=card n, i-й коэффициент универсального полинома однороден по степени j.

LaTeX

$$∀ i j, (i + j = Fintype.card n) → ((\\mathrm{charpoly.univ}\\,R\\,n).\\operatorname{coeff} i).IsHomogeneous j$$

Lean4

theorem univ_coeff_isHomogeneous (i j : ℕ) (h : i + j = Fintype.card n) : ((univ R n).coeff i).IsHomogeneous j :=
  (optionEquivLeft_symm_univ_isHomogeneous R n).coeff_isHomogeneous_of_optionEquivLeft_symm _ _ h

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