Theorems · Theorem · number theory

NumberField.mixedEmbedding.adjust_f

∀ (K : Type u_1) [inst : Field K] {f : NumberField.InfinitePlace K → NNReal} [inst_1 : NumberField K]
  {w₁ : NumberField.InfinitePlace K} (B : NNReal),
  (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → f w ≠ 0) →
    ∃ g, (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w, g w ^ w.mult = B

This is a technical result: quite often, we want to impose conditions at all infinite places but one and choose the value at the remaining place so that we can apply exists_ne_zero_mem_ringOfIntegers_lt.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField