Commit 2022-09-30 23:37 7aebb349

refactor(ring_theory/polynomial/tower): review APIs (#16678) Split from #16412. All of the following lemmas move from namespace is_scalar_tower to namespace polynomial. Rename aeval_apply to aeval_map_algebra_map and swap the sides of the equality, remove aeval_map which is just the same as aeval_map_algebra_map. Rename algebra_map_aeval to aeval_algebra_map_apply and swap the sides of the equality, rename original aeval_algebra_map_apply to aeval_algebra_map_apply_eq_algebra_map_eval. Make the new lemma a simp lemma and remove simp from the original one. Rename aeval_eq_zero_of_aeval_algebra_map_eq_zero to aeval_algebra_map_eq_zero_iff_of_injective and make it an iff lemma. Replace aeval_eq_zero_of_aeval_algebra_map_eq_zero_field by aeval_algebra_map_eq_zero_iff, it has weaker assumptions and is also an iff lemma.

• depends on: #16673