Theorems · Theorem · number theory

Height.mulHeight_linearMap_apply_le

∀ {K : Type u_1} [inst : Field K] {ι : Type u_2} {ι' : Type u_3} [inst_1 : Fintype ι] [Finite ι']
  [inst_3 : Height.AdmissibleAbsValues K] [Nonempty ι] (A : ι' × ι → K) (x : ι → K),
  (Height.mulHeight fun j => ∑ i, A (j, i) * x i) ≤
    ↑(Nat.card ι) ^ Height.totalWeight K * Height.mulHeight A * Height.mulHeight x

Let A : ι' × ι → K, which we can interpret as a linear map from ι → K to ι' → K. Let x : ι → K be a tuple. Then the multiplicative height of A x is bounded by #ι ^ totalWeight K * mulHeight A * mulHeight x (if ι is nonempty). Note: We use the uncurried form of A so that we can write mulHeight A.

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

FieldFintypeFiniteHeight.AdmissibleAbsValuesNonempty