∀ {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]
  (φ φ_1 : L →ₗ[R] Module.End R M),
  φ = φ_1 →
    ∀ [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι] {inst_8 : DecidableEq ιM}
      [inst_9 : DecidableEq ιM] (b b_1 : Module.Basis ι R L),
      b = b_1 → ∀ (bₘ bₘ_1 : Module.Basis ιM R M), bₘ = bₘ_1 → φ.polyCharpolyAux b bₘ = φ_1.polyCharpolyAux b_1 bₘ_1