Theorems · Theorem · number theory

NumberField.absNorm_mul_finprod_finitePlace_eq_one

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {ι : Type u_2} [Finite ι]
  {x : ι → NumberField.RingOfIntegers K},
  x ≠ 0 → ↑(Ideal.absNorm (Ideal.span (Set.range x))) * ∏ᶠ (v : NumberField.FinitePlace K), ⨆ i, v ↑(x i) = 1

This statement is equivalent to the fact that the "finite part" of the multiplicative height of a (non-zero) tuple x is the inverse of the absolute norm of the ideal generated by the values of x. We state it in a way that avoids taking an inverse.

Defined in

Mathlib.NumberTheory.Height.NumberField

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberFieldFinite