Theorems · Theorem · number theory

Height.mulHeight_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.mulHeight fun a => x a.1 * y a.2) = Height.mulHeight x * Height.mulHeight y

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

Defined in

Mathlib.NumberTheory.Height.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValuesFiniteFinite