Theorems · Theorem · number theory

NumberField.Units.dirichletUnitTheorem.seq.congr_simp

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ w₁_1 : NumberField.InfinitePlace K),
  w₁ = w₁_1 →
    ∀ {B B_1 : ℕ} (e_B : B = B_1)
      (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B)
      (a a_1 : ℕ),
      a = a_1 →
        NumberField.Units.dirichletUnitTheorem.seq K w₁ hB a = NumberField.Units.dirichletUnitTheorem.seq K w₁_1 ⋯ a_1

Defined in

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldNumberField