Theorems · Theorem · number theory

Ideal.ncard_primesOver_mul_card_inertia_mul_finrank

∀ {R : Type u_1} {S : Type u_2} {G : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] (p : Ideal R)
  [inst_7 : p.IsPrime] (P : Ideal S) [P.LiesOver p] [P.IsPrime] [PerfectField p.ResidueField],
  (p.primesOver S).ncard * Nat.card ↥(Ideal.inertia G P) * P.inertiaDeg R = Nat.card G

Defined in

Mathlib.NumberTheory.RamificationInertia.Galois

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraGroupMulSemiringActionIsGaloisGroupFiniteIdeal.IsPrimeIdeal.LiesOverIdeal.IsPrimePerfectField