Theorems · Theorem · number theory

NumberField.Units.map_complexEmbedding_torsion

∀ (K : Type u_1) [inst : Field K] [NumberField K] (φ : K →+* ℂ),
  Subgroup.map (NumberField.Units.complexEmbedding φ) (NumberField.Units.torsion K) =
    rootsOfUnity (NumberField.Units.torsionOrder K) ℂ

The image of torsion K by a complex embedding is the group of complex roots of unity of order torsionOrder K.

Defined in

Mathlib.NumberTheory.NumberField.Units.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField