theorem Eigenvalues.eigenvalue_iff_root_charPoly {n : Type u_1} [Fintype n] [DecidableEq n] {F : Type u_2} [Field F] (A : Matrix n n F) (μ : F) : μ ∈ spectrum F A ↔ A.charpoly.IsRoot μ

theorem Eigenvalues.eigenvectors_linearIndependent {ι : Type u_3} {R : Type u_4} {M : Type u_5} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] (f : Module.End R M) (μ : ι → R) (hμ : Function.Injective μ) (v : ι → M) (h_eigenvec : ∀ (i : ι), f.HasEigenvector (μ i) (v i)) : LinearIndependent R v