Theorems · Theorem · number theory

Height.mulHeightBound_eq

∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K]
  (p : ι' → MvPolynomial ι K),
  Height.mulHeightBound p =
    (Multiset.map (fun v => ⨆ j, (p j).coeff.sum fun x c => v c) Height.AdmissibleAbsValues.archAbsVal).prod *
      ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (MvPolynomial.coeff (↑s) (p j))) 1

Defined in

Mathlib.NumberTheory.Height.MvPolynomial

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValues