Theorem Module.Basis.coe_mkFinSnoc

Modification history

2026-04-27 13:42

Mathlib/LinearAlgebra/Basis/Fin.lean

feat(LinearAlgebra/Basis/Fin): linear independence of `Fin.snoc` (#37810) …

Added Module.Basis.coe_mkFinSnoc View on Github →