Theorems · Theorem · number theory

Ideal.quotientToQuotientRangePowQuotSucc_surjective

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)
  [hfp : NeZero (p.ramificationIdx' P)] [IsDedekindDomain S],
  P ≠ ⊥ →
    ∀ [hP : P.IsPrime] {i : ℕ},
      i < p.ramificationIdx' P →
        ∀ {a : S} (a_mem : a ∈ P ^ i),
          a ∉ P ^ (i + 1) → Function.Surjective ⇑(p.quotientToQuotientRangePowQuotSucc P a_mem)

Defined in

Mathlib.NumberTheory.RamificationInertia.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraNeZeroIsDedekindDomainIdeal.IsPrime