Theorem coe_basisOfPiSpaceOfLinearIndependent

Modification history

2026-04-27 13:42
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean
feat(LinearAlgebra/Basis/Fin): linear independence of `Fin.snoc` (#37810) …
Modified coe_basisOfPiSpaceOfLinearIndependentView on Github →
2025-03-23 09:06
Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean
feat(LinearAlgebra/FiniteDimensional): add `basisOfPiSpaceOfLinearIndependent` (#22868) …
Added coe_basisOfPiSpaceOfLinearIndependentView on Github →