Theorem Module.End.eigenvectors_linearIndependent'

Modification history

2026-01-13 19:40

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Modified Module.End.eigenvectors_linearIndependent'View on Github →

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 →