Theorems · Theorem · number theory

Height.mulHeight_mul_mulHeight

∀ {K : Type u_4} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {a b c d : K},
  ![a, b] ≠ 0 →
    ![c, d] ≠ 0 → 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

2 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValues