Theorems · Theorem · number theory

IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd

∀ {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [NeZero m]
  [hK : IsCyclotomicExtension {m} ℚ K], ¬p ∣ m → (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = 1

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactFieldNumberFieldNeZeroIsCyclotomicExtension