IsNilRegular — Mathlib

English

There exists an x with IsNilRegular φ x when finrank constraints hold; otherwise stated in a more general setting.

Русский

Существует x с IsNilRegular φ x при выполнении ограничений на размерность; иначе сказано в общем виде.

LaTeX

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

Lean4

/-- Let `L` and `M` be finite free modules over `R`,
and let `φ : L →ₗ[R] Module.End R M` be a linear family of endomorphisms,
and denote `n := nilRank φ`.

An element `x : L` is *nil-regular* with respect to `φ`
if the `n`-th coefficient of the characteristic polynomial of `φ x` is non-zero. -/
def IsNilRegular (x : L) : Prop :=
  Polynomial.coeff (φ x).charpoly (nilRank φ) ≠ 0

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