Theorems · Theorem · number theory

Height.logHeight_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.logHeight (x ∘ f) ≤ Height.logHeight x

Defined in: Mathlib.NumberTheory.Height.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Height.AdmissibleAbsValues Finite Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
Fieldstatement and proof · cited by 7,404
Finitestatement and proof · cited by 3,029
Height.AdmissibleAbsValuesstatement and proof · cited by 110
Real.log_le_logproof · cited by 39
Height.logHeightstatement · cited by 35
Height.mulHeight_posproof · cited by 13
Height.mulHeight_comp_leproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.