Commit 2025-05-12 14:24 4ba09b1a

View on Github →

chore(Multilinear/Basis): golf, generalize (#24802)

Estimated changes

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basis.lean

modified theorem Basis.ext_multilinear

deleted theorem Basis.ext_multilinear_fin