Commit 2022-04-05 11:06 220f71ba

refactor(data/polynomial/basic): overhaul all the misnamed to_finsupp lemmas (#13139) zero_to_finsupp was the statement of_finsupp 0 = 0, which doesn't match the name at all. This change:

• Renames all those lemmas to of_finsupp_<foo>
• Changes the direction of add_to_finsupp to be of_finsupp_add, so the statement is now of_finsupp (a + b) = _
• Adds the missing to_finsupp_<foo> lemmas
• Uses the new lemmas to golf the semiring and ring instances The renames include:
• zero_to_finsupp → of_finsupp_zero
• one_to_finsupp → of_finsupp_one
• add_to_finsupp → of_finsupp_add (direction reversed)
• neg_to_finsupp → of_finsupp_neg (direction reversed)
• mul_to_finsupp → of_finsupp_mul (direction reversed)
• smul_to_finsupp → of_finsupp_smul (direction reversed)
• sum_to_finsupp → of_finsupp_sum (direction reversed)
• to_finsupp_iso_monomial → to_finsupp_monomial
• to_finsupp_iso_symm_single → of_finsupp_single
• eval₂_to_finsupp_eq_lift_nc → eval₂_of_finsupp The new lemmas include:
• of_finsupp_sub
• of_finsupp_pow
• of_finsupp_erase
• of_finsupp_algebra_map
• of_finsupp_eq_zero
• of_finsupp_eq_one
• to_finsupp_zero
• to_finsupp_one
• to_finsupp_add
• to_finsupp_neg
• to_finsupp_sub
• to_finsupp_mul
• to_finsupp_pow
• to_finsupp_erase
• to_finsupp_algebra_map
• to_finsupp_eq_zero
• to_finsupp_eq_one
• to_finsupp_C Note that by marking things like support and coeff as @[simp], they behave as if they were support_of_finsupp or coeff_of_finsupp lemma. By making coeff pattern match fewer arguments, we encourage it to apply more keenly. Neither lemma will fire unless our expression contains polynomial.of_finsupp.