Commit 2022-08-03 11:38 798b4ae1

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.