Theorems · Theorem · commutative algebra

MixedCharZero.reduce_to_maximal_ideal

∀ (R : Type u_1) [inst : CommRing R] {p : ℕ},
  Nat.Prime p → ((∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p)

Reduction to I prime ideal: When proving statements about mixed characteristic rings, after we reduced to p prime, we can assume that the ideal I in the definition is maximal.

Defined in

Mathlib.Algebra.CharP.MixedCharZero

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing