Theorems · Theorem · linear algebra

LinearMap.charpoly_prodMap

∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Module.Finite R M₁] [inst_4 : Module.Free R M₁] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  [inst_7 : Module.Finite R M₂] [inst_8 : Module.Free R M₂] (f₁ : M₁ →ₗ[R] M₁) (f₂ : M₂ →ₗ[R] M₂),
  (f₁.prodMap f₂).charpoly = f₁.charpoly * f₂.charpoly

Defined in

Mathlib.LinearAlgebra.Charpoly.ToMatrix

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleModule.FiniteModule.FreeAddCommGroupModuleModule.FiniteModule.Free