Theorems · Theorem · number theory

Height.mulHeight_sym2_ge

∀ (K : Type u_4) [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K],
  ∃ C > 0,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 →
          C * Height.mulHeight ![a, b] * Height.mulHeight ![c, d] ≤ Height.mulHeight ![a * c, a * d + b * c, b * d]

Defined in

Mathlib.NumberTheory.Height.MvPolynomial

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValues