Commit 2026-04-27 13:42 b2e2aab8
View on Github →feat(LinearAlgebra/Basis/Fin): linear independence of Fin.snoc (#37810)
In #37740 we renamed several LinearIndependent lemmas from names such as fin_cons to camelCase, e.g., finCons. Missing from this collection of lemmas was finSnoc and some related lemmas that are useful for certain inductions.
This PR adds these extra lemmas and constructions to mathlib.