Theorems · Theorem · number theory

NumberField.Units.mem_torsion

∀ (K : Type u_1) [inst : Field K] [NumberField K] {x : (NumberField.RingOfIntegers K)ˣ},
  x ∈ NumberField.Units.torsion K ↔
    ∀ (w : NumberField.InfinitePlace K), w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x) = 1

Defined in

Mathlib.NumberTheory.NumberField.Units.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldNumberField