Theorems · Theorem · number theory

Height.mulHeight_comp_le

∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
  [Finite ι'] (f : ι → ι') (x : ι' → K), Height.mulHeight (x ∘ f) ≤ Height.mulHeight x

Defined in

Mathlib.NumberTheory.Height.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValuesFiniteFinite