Theorems · Theorem · number theory

Height.mulHeight_pow

∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (n : ℕ),
  Height.mulHeight (x ^ n) = Height.mulHeight x ^ n

The multiplicative height of the coordinate-wise nth power of a tuple is the nth power of its multiplicative height.

Defined in

Mathlib.NumberTheory.Height.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValuesFinite