…otte bound

Extract Landau's inequality as a standalone theorem: the Mahler measure
of a polynomial is at most the ℓ² norm of its coefficient vector. This
was previously an intermediate step inside the proof of
`mahlerMeasure_le_sqrt_natDegree_add_one_mul_supNorm`.

Also add:
- `one_le_mahlerMeasure`: M(p) ≥ 1 when the leading coefficient has
  norm ≥ 1 (e.g. nonzero integer polynomials)
- `le_mahlerMeasure_mul_right/left`: monotonicity of Mahler measure
  under multiplication by a polynomial with M ≥ 1
- `norm_coeff_le_choose_mul_mahlerMeasure_mul`: Mignotte's coefficient
  bound for factors — if f = g * h with M(h) ≥ 1, then
  ‖g.coeff n‖ ≤ C(deg g, n) · M(f)

These results complete the Mahler measure toolkit needed for verified
polynomial factorization (Berlekamp–Zassenhaus).

Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>

- Rename `one_le_mahlerMeasure` to `one_le_mahlerMeasure_of_one_le_norm_leadingCoeff`
  to follow Mathlib convention of encoding hypotheses in names (matching
  the existing `one_le_mahlerMeasure_of_ne_zero` in NumberTheory).
- Rename `norm_coeff_le_choose_mul_mahlerMeasure_mul` to
  `norm_coeff_le_choose_mul_mahlerMeasure_of_one_le_mahlerMeasure`
  since the `_mul` suffix was misleading (reads as multiplicativity).
- Replace informal `‖f‖₂` in Mignotte docstring with the explicit
  `√(∑ i ∈ f.support, ‖f.coeff i‖ ^ 2)`.
- Differentiate docstrings for `le_mahlerMeasure_mul_left` vs `_right`.

Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>