Theorems · Definition · number theory

Ideal.Factors.piQuotientEquiv

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] →
          [inst_3 : IsDedekindDomain S] →
            (p : Ideal R) →
              Ideal.map (algebraMap R S) p ≠ ⊥ →
                S ⧸ Ideal.map (algebraMap R S) p ≃+*
                  ((P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset) →
                    S ⧸ ↑P ^ p.ramificationIdx' ↑P)

Chinese remainder theorem for a ring of integers: if the prime ideal p : Ideal R factors in S as ∏ i, P i ^ e i, then S ⧸ I factors as Π i, R ⧸ (P i ^ e i).

Defined in

Mathlib.NumberTheory.RamificationInertia.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDedekindDomain