Commit 2022-09-25 18:26 5a8eded1

refactor(linear_algebra/affine_space): remove open_locale classical (#16628) Use of open_locale classical in mathlib is liable to cause problems if it results in the classical decidability instances forming part of the type of a lemma, making that lemma harder to use in any context where typeclass inference finds a different decidability instance. Remove it from affine space files, adding explicit decidability instance parameters where needed for the type of a lemma and uses of the classical tactic when only needed for a proof.