mathlib3

798b4ae1 - refactor(linear_algebra): morphism refactor for `linear_equiv`, `continuous_linear_equiv`, `linear_isometry` and `linear_isometry_equiv` (#15078)

refactor(linear_algebra): morphism refactor for `linear_equiv`, `continuous_linear_equiv`, `linear_isometry` and `linear_isometry_equiv` (#15078) This PR brings the morphism refactor to `linear_equiv`, `continuous_linear_equiv`, `linear_isometry`, and `linear_isometry_equiv`. Note that I had to resort to an ugly hack to deal with deterministic timouts in two proofs: `vitali.exists_disjoint_covering_ae` and another one in the counterexamples folder. Both of these are very large proofs with no obvious sublemmas to extract or inefficiencies, so I just used `try_for 20000 {...}` to increase the timeout. It's not great, but I don't see a better alternative -- besides, I don't think it's unreasonable for long proofs like these to have a bigger timeout. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>