Theorems · Definition · linear algebra

LinearMap.nilRankAux

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

(Implementation detail, see LinearMap.nilRank.) Let L and M be finite free modules over R, and let φ : L →ₗ[R] Module.End R M be a linear family of endomorphisms. Then LinearMap.nilRankAux φ b is the smallest index at which LinearMap.polyCharpoly φ b has a non-zero coefficient. This number does not depend on the choice of b, see nilRankAux_basis_indep.

Defined in

Mathlib.Algebra.Module.LinearMap.Polynomial

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleFintypeDecidableEqModule.FreeModule.Finite