mathlib

06930844 - refactor(linear_algebra/affine_space/finite_dimensional): change three lemmas to instances (#16331)

refactor(linear_algebra/affine_space/finite_dimensional): change three lemmas to instances (#16331) I realised after the PR with these lemmas was approved that they are actually suitable to be instances (don't depend on any hypotheses that typeclass inference can't deduce), and making them such sometimes allows removing explicit `haveI` uses because typeclass inference can then find them automatically.