Theorems · Theorem · number theory

NumberField.torsionOrder_dvd_absNorm_sub_one

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {P : Ideal (NumberField.RingOfIntegers K)},
  P ≠ ⊥ →
    P.IsPrime →
      (Ideal.absNorm P).Coprime (NumberField.Units.torsionOrder K) →
        NumberField.Units.torsionOrder K ∣ Ideal.absNorm P - 1

If the norm of the (nonzero) prime ideal P is coprime with the order of the torsion of K, then the norm of P is congruent to 1 modulo torsionOrder K.

Defined in

Mathlib.NumberTheory.NumberField.Ideal.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldNumberField