Theorems · Definition · number theory

NumberField.IsCMField.unitsMulComplexConjInv

(K : Type u_1) →
  [inst : Field K] →
    [inst_1 : CharZero K] →
      [NumberField.IsCMField K] → [NumberField K] → (NumberField.RingOfIntegers K)ˣ →* ↥(NumberField.Units.torsion K)

The map (𝓞 K)ˣ →* torsion K defined by u ↦ u * (conj u)⁻¹.

Defined in

Mathlib.NumberTheory.NumberField.CMField

Cited by

9 results in Mathlib

Foundations

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

Assumes

FieldCharZeroNumberField.IsCMFieldNumberField