mathlib

f2edd790 - fix(linear_algebra/basis): add missing decidable arguments in lemmas (#18252)

fix(linear_algebra/basis): add missing decidable arguments in lemmas (#18252) The resulting lemmas are syntactically more general. To ensure that this catches all of them, this also removes `open_locale classical` from the file, replacing it with manual construction of classical decidability instances within definitions, and `classical` within proofs.