Theorem Module.End.eigenvectors_linearIndependent'

Modification history

2024-08-01 14:36
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
feat: Adds a variant of lemma about eigenvectors. (#15404)
Added Module.End.eigenvectors_linearIndependent'View on Github →