mathlib3

9893a260 - chore(field_theory/splitting_field): module doc and generalise one lemma (#6739)

chore(field_theory/splitting_field): module doc and generalise one lemma (#6739) This PR provides a module doc for `field_theory.splitting_field`, which is the last file without module doc in `field_theory`. Furthermore, I took the opportunity of renaming the fields in that file from `\alpha`, `\beta`, `\gamma` to `K`, `L`, `F` to make it more readable for newcomers. Moved `nat_degree_multiset_prod`, to `algebra.polynomial.big_operators`). In order to get the `no_zero_divisors` instance on `polynomial R`, I had to include `data.polynomial.ring_division` in that file. Furthermore, with the help of Damiano, generalised this lemma to `no_zero_divisors R`. Coauthored by: Damiano Testa adomani@gmail.com Co-authored-by: Thomas Browning <tb65536@uw.edu> Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>