Theorems · Theorem · number theory

Height.mulHeight_eq

∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {x : ι → K},
  x ≠ 0 →
    Height.mulHeight x =
      (Multiset.map (fun v => ⨆ i, v (x i)) Height.AdmissibleAbsValues.archAbsVal).prod *
        ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), ⨆ i, ↑v (x i)

Defined in

Mathlib.NumberTheory.Height.Basic

Cited by

14 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValues