Theorems · Theorem · linear algebra

LinearMap.charpoly_toMatrix

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M) {ι : Type w} [inst_5 : DecidableEq ι]
  [inst_6 : Fintype ι] (b : Module.Basis ι R M), ((LinearMap.toMatrix b b) f).charpoly = f.charpoly

charpoly f is the characteristic polynomial of the matrix of f in any basis.

Defined in

Mathlib.LinearAlgebra.Charpoly.ToMatrix

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleModule.FreeModule.FiniteDecidableEqFintype