∀ {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