Commit 2021-03-04 11:33 deb3d452

feat(data/mv_polynomial/equiv): generalize ring_equiv_congr (#6420) Following the discussion in #6324, I have modified mv_polynomial.ring_equiv_of_equiv and mv_polynomial.ring_equiv_congr, that are now called ring_equiv_congr_left and ring_equiv_congr_left: both are proved as special cases of ring_equiv_congr (the situation for algebras is exactly the same). This has the side effect that the lemmas automatically generated by @[simps] are not in a good form (see for example the lemma mv_polynomial.alg_equiv_congr_left_apply in the current mathlib, where there is an unwanted alg_equiv.refl.to_ring_equiv). To avoid this I deleted the @[simps] and I wrote the lemmas by hand (also correcting the problem with mv_polynomial.alg_equiv_congr_left_apply). I probably don't understand completely @[simps], since I had to manually modified some other proofs that no longer worked (I mean, I had to do something more that just using the new names). If there is some simp lemma I forgot I would be happy to write it.