Commit 2021-03-09 21:43 8e246cbb

refactor(data/mv_polynomial): cleanup equivs (#6589) This:

• Replaces alg_equiv_congr_left with rename_equiv (to match rename)
• Removes ring_equiv_congr_left (it's now rename_equiv.to_ring_equiv)
• Renames alg_equiv_congr_right to map_alg_equiv (to match map) and removes the comap from the definition
• Renames ring_equiv_congr_right to map_equiv (to match map)
• Removes alg_equiv_congr (it's now (map_alg_equiv R e).trans $ (rename_equiv e_var).restrict_scalars _, which while longer is never used anyway)
• Removes ring_equiv_congr (it's now (map_equiv R e).trans $ (rename_equiv e_var).to_ring_equiv, which while longer is never used anyway)
• Replaces punit_ring_equiv with punit_alg_equiv
• Removes comap from the definition of sum_alg_equiv
• Promotes option_equiv_left, option_equiv_right, and fin_succ_equiv to alg_equivs This is a follow-up to #6420