Theorems · Definition · linear algebra

LinearMap.polyCharpolyAux

{R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      {ι : Type u_5} →
        {ιM : Type u_7} →
          [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) →
                      [Fintype ι] →
                        [Fintype ιM] →
                          [DecidableEq ι] →
                            [DecidableEq ιM] → Module.Basis ι R L → Module.Basis ιM R M → Polynomial (MvPolynomial ι R)

(Implementation detail, see LinearMap.polyCharpoly.) Let L and M be finite free modules over R, and let φ : L →ₗ[R] Module.End R M be a linear map. Let b be a basis of L and bₘ a basis of M. Then LinearMap.polyCharpolyAux φ b bₘ is the polynomial that evaluates on elements x of L to the characteristic polynomial of φ x acting on M. This definition does not depend on the choice of bₘ (see LinearMap.polyCharpolyAux_basisIndep).

Defined in

Mathlib.Algebra.Module.LinearMap.Polynomial

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleFintypeFintypeDecidableEqDecidableEq