Theorems · Theorem · number theory

NumberField.mulHeight_eq

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {ι : Type u_2} {x : ι → K},
  x ≠ 0 → Height.mulHeight x = (∏ v, (⨆ i, v (x i)) ^ v.mult) * ∏ᶠ (v : NumberField.FinitePlace K), ⨆ i, v (x i)

This is the familiar definition of the multiplicative height on (nonzero) tuples of number field elements.

Defined in

Mathlib.NumberTheory.Height.NumberField

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldNumberField