nilRank_le_natTrailingDegree_charpoly

English

If finrank R M ≤ #R, there exists x ∈ L such that IsNilRegular φ x; equivalently, there exists a nil-regular element.

Русский

Если finrank_R M не больше числа кардиналов R, существует x ∈ L такое, что IsNilRegular φ x; иначе говоря, существует элемент, nil-регулярный по отношению к φ.

LaTeX

$$∃ x : L, IsNilRegular φ x$$

Lean4

theorem nilRank_le_natTrailingDegree_charpoly (x : L) : nilRank φ ≤ (φ x).charpoly.natTrailingDegree :=
  by
  apply Polynomial.natTrailingDegree_le_of_ne_zero
  intro h
  apply_fun (MvPolynomial.eval ((chooseBasis R L).repr x)) at h
  rw [polyCharpoly_coeff_eval, map_zero] at h
  apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr _ h
  apply (LinearMap.charpoly_monic _).ne_zero

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