Theorems · Theorem · number theory

Height.logHeight_fun_mul_eq

∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
  [Finite ι'] {x : ι → K},
  x ≠ 0 → ∀ {y : ι' → K}, y ≠ 0 → (Height.logHeight fun a => x a.1 * y a.2) = Height.logHeight x + Height.logHeight y

The logarithmic height of the "multiplication table" fun (i, j) ↦ x i * y j is the sum of the logarithmic heights of x and y.

Defined in

Mathlib.NumberTheory.Height.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValuesFiniteFinite