Commit 2023-01-22 01:07 f2edd790

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.