mathlib

5a8eded1 - refactor(linear_algebra/affine_space): remove `open_locale classical` (#16628)

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.