isNilRegular_def — Mathlib

English

An element x ∈ L is called nil-regular with respect to φ if the nth coefficient of the charpoly of φ x is nonzero, where n is nilRank φ.

Русский

Элемент x ∈ L называется nil-regular относительно φ, если коэффициент при индексе n = nilRank φ в характеристическом полиномe φ x не равен нулю.

LaTeX

$$IsNilRegular φ x := Polynomial.coeff (φ x).charpoly (nilRank φ) ≠ 0$$

Lean4

theorem isNilRegular_def : IsNilRegular φ x ↔ (Polynomial.coeff (φ x).charpoly (nilRank φ) ≠ 0) :=
  Iff.rfl

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