Theorems · Theorem · number theory

Ideal.finrank_prime_pow_ramificationIdx

Deprecated since 2026-07-01Mathlib marks this declaration as deprecated.

∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [IsDedekindDomain S],
  P ≠ ⊥ →
    ∀ [p.IsMaximal] [P.IsPrime] (he : p.ramificationIdx' P ≠ 0),
      Module.finrank (R ⧸ p) (S ⧸ P ^ p.ramificationIdx' P) = p.ramificationIdx' P * Module.finrank (R ⧸ p) (S ⧸ P)

If p is a maximal ideal of R, S extends R and P^e lies over p, then the dimension [S/(P^e) : R/p], as a natural number, is equal to e * [S/P : R/p].

Defined in

Mathlib.NumberTheory.RamificationInertia.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDedekindDomainIdeal.IsMaximalIdeal.IsPrime