basic): Remove references to `polynomial.norm2` (#13847)

Commit

3 years ago

doc(data/polynomial/basic): Remove references to `polynomial.norm2` (#13847) `polynomial.norm2` was never added to mathlib.

Author

tb65536

Parents