Theorems · Definition · linear algebra

LinearMap.IsNilRegular

{R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup L] →
          [inst_2 : Module R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                (L →ₗ[R] Module.End R M) →
                  [Module.Free R M] → [Module.Finite R M] → [Module.Finite R L] → [Module.Free R L] → L → Prop

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.

Defined in

Mathlib.Algebra.Module.LinearMap.Polynomial

Cited by

5 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleModule.FreeModule.FiniteModule.FiniteModule.Free