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.
- [x] depends on: #16673
