Commit 2026-04-09 12:35 644bbfd5

View on Github →

chore: rename fin_cons etc to finCons (#37740) LinearIndependent.fin_cons and its ilk fin_cons' fin_succ and fin_succ' had not been updated to use camelCase. This commit fixes all instances of this. We also fix a typo whereby an element y was defined by y : Submodule.span instead of (y : M), y \in Submodule.span.

Estimated changes

Modified Mathlib/LinearAlgebra/Basis/Fin.lean

Modified Mathlib/LinearAlgebra/Basis/Submodule.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

added theorem LinearIndependent.finCons'

deleted theorem LinearIndependent.fin_cons'

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

added theorem LinearIndependent.finCons

deleted theorem LinearIndependent.fin_cons

added theorem linearIndependent_finCons

added theorem linearIndependent_finSnoc

added theorem linearIndependent_finSucc'

added theorem linearIndependent_finSucc

deleted theorem linearIndependent_fin_cons

deleted theorem linearIndependent_fin_snoc

deleted theorem linearIndependent_fin_succ'

deleted theorem linearIndependent_fin_succ

Modified Mathlib/RingTheory/Polynomial/Bernstein.lean