doc(data/polynomial/basic): Remove references to polynomial.norm2 (#…

…13847)

`polynomial.norm2` was never added to mathlib.

src/data/polynomial/mirror.lean

@@ -11,19 +11,16 @@ import data.polynomial.ring_division
 
 In this file we define `polynomial.mirror`, a variant of `polynomial.reverse`. The difference
 between `reverse` and `mirror` is that `reverse` will decrease the degree if the polynomial is
-divisible by `X`. We also define `polynomial.norm2`, which is the sum of the squares of the
-coefficients of a polynomial. It is also a coefficient of `p * p.mirror`.
+divisible by `X`.
 
 ## Main definitions
 
 - `polynomial.mirror`
-- `polynomial.norm2`
 
 ## Main results
 
 - `polynomial.mirror_mul_of_domain`: `mirror` preserves multiplication.
 - `polynomial.irreducible_of_mirror`: an irreducibility criterion involving `mirror`
-- `polynomial.norm2_eq_mul_reverse_coeff`: `norm2` is a coefficient of `p * p.mirror`
 
 -/