Theorems · Theorem · number theory

NumberField.Units.dirichletUnitTheorem.logEmbedding_component

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : (NumberField.RingOfIntegers K)ˣ)
  (w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  (NumberField.Units.logEmbedding K) (Additive.ofMul x) w =
    ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x))

Defined in

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldNumberField