Theorems · Theorem · number theory

KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S],
  I.IsMaximal →
    I ≠ ⊥ →
      Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
        IsIntegral R x →
          Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) → Irreducible (Ideal.map (algebraMap R S) I)

Defined in

Mathlib.NumberTheory.KummerDedekind

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDomainIsIntegrallyClosedIsDedekindDomainModule.IsTorsionFree