Theorems · Theorem · number theory

Ideal.ncard_primesOver_mul_ncard_primesOver

∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [FaithfulSMul A B]
  {p : Ideal A} (P : Ideal B) [P.IsPrime] [P.LiesOver p] (G : Type u_3) [inst_6 : Group G] [Finite G]
  [inst_8 : MulSemiringAction G B] [IsGaloisGroup G A B] (C : Type u_4) [inst_10 : CommRing C] [IsDomain C]
  [inst_12 : Algebra A C] [inst_13 : Algebra B C] [FaithfulSMul B C] [IsScalarTower A B C] (GAC : Type u_5)
  [inst_16 : Group GAC] [Finite GAC] [inst_18 : MulSemiringAction GAC C] [IsGaloisGroup GAC A C],
  (p.primesOver B).ncard * (P.primesOver C).ncard = (p.primesOver C).ncard

Defined in

Mathlib.NumberTheory.RamificationInertia.Galois

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFaithfulSMulIdeal.IsPrimeIdeal.LiesOverGroupFiniteMulSemiringActionIsGaloisGroupCommRingIsDomainAlgebraAlgebraFaithfulSMulIsScalarTowerGroupFiniteMulSemiringActionIsGaloisGroup