Commit 2024-09-11 04:48 0e1a0b8d

chore: remove variables from LinearAlgebra.FreeModule.Finite.Basic (#16662) The current setup with an unused variable (N) and one theorem overriding the ambient variables, as well as a namespace that's explicitly overridden in two of the three results within it, is confusing. It is clearer to explicitly spell out the arguments to each declaration.