chore(data/polynomial/expand): update docstrings for move (#16044)

Ref: #13776.

src/data/polynomial/expand.lean

@@ -9,6 +9,13 @@ import tactic.ring_exp
 
 /-!
 # Expand a polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`.
+
+## Main definitions
+
+* `polynomial.expand R p f`: expand the polynomial `f` with coefficients in a
+  commutative semiring `R` by a factor of p, so `expand R p (∑ aₙ xⁿ)` is `∑ aₙ xⁿᵖ`.
+* `polynomial.contract p f`: the opposite of `expand`, so it sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`.
+
 -/
 
 universes u v w

src/field_theory/separable.lean

@@ -20,9 +20,6 @@ properties about separable polynomials here.
 ## Main definitions
 
 * `polynomial.separable f`: a polynomial `f` is separable iff it is coprime with its derivative.
-* `polynomial.expand R p f`: expand the polynomial `f` with coefficients in a
-  commutative semiring `R` by a factor of p, so `expand R p (∑ aₙ xⁿ)` is `∑ aₙ xⁿᵖ`.
-* `polynomial.contract p f`: the opposite of `expand`, so it sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`.
 
 -/