Theorems · Theorem · number theory

Ideal.absNorm_eq_pow_inertiaDeg

∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R] [Module.Finite ℤ R] {p : ℤ}
  (P : Ideal R) [P.LiesOver (Ideal.span {p})], Prime p → Ideal.absNorm P = p.natAbs ^ (Ideal.span {p}).inertiaDeg' P

The absolute norm of an ideal P above a rational prime p is |p| ^ ((span {p}).inertiaDeg' P). See absNorm_eq_pow_inertiaDeg' for a version with p of type ℕ.

Defined in

Mathlib.NumberTheory.RamificationInertia.Inertia

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainModule.FreeModule.FiniteIdeal.LiesOver