Theorems · Theorem · number theory

Height.mulHeight_eval_le

∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K] [Finite ι']
  [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K},
  (∀ (i : ι'), (p i).IsHomogeneous N) →
    ∀ (x : ι → K),
      (Height.mulHeight fun j => (MvPolynomial.eval x) (p j)) ≤ max (Height.mulHeightBound p) 1 * Height.mulHeight x ^ N

Let K be a field with an admissible family of absolute values (giving rise to a multiplicative height). Let p be a family (indexed by ι') of homogeneous polynomials in variables indexed by the finite type ι and of the same degree N. Then for any x : ι → K, the multiplicative height of fun j : ι' ↦ eval x (p j) is bounded by a positive constant (which is made explicit) times mulHeight x ^ N.

Defined in

Mathlib.NumberTheory.Height.MvPolynomial

Cited by

3 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldHeight.AdmissibleAbsValuesFiniteFinite