Theorems · Definition · number theory

RingOfIntegers.exponent

{K : Type u_1} → [inst : Field K] → NumberField.RingOfIntegers K → ℕ

The smallest positive integer d contained in the conductor of θ. It is the smallest integer such that d • 𝓞 K ⊆ ℤ[θ], see exponent_eq_sInf. It is set to 0 if d does not exists.

Defined in

Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Cited by

15 results in Mathlib

Foundations

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

Assumes

Field