polyCharpoly_coeff_nilRankAux_ne_zero

English

The coefficient of polyCharpoly φ b at the index nilRankAux φ b is nonzero.

Русский

Коэффициент полинома polyCharpoly φ b при индексе nilRankAux φ b ненулевой.

LaTeX

$$((\mathrm{polyCharpoly } φ b).\mathrm{coeff} (\mathrm{nilRankAux } φ b)) \neq 0$$

Lean4

theorem polyCharpoly_coeff_nilRankAux_ne_zero [Nontrivial R] : (polyCharpoly φ b).coeff (nilRankAux φ b) ≠ 0 :=
  by
  apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr
  apply polyCharpoly_ne_zero

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