of_not_mixedCharZero — Mathlib

English

If all quotients have CharZero, then D is not mixed characteristic for any p.

Русский

Если все фактор-кольца имеют CharZero, то характеристика D не смешанная для любого p.

LaTeX

$$$\\forall I, I \\neq \\top \\Rightarrow CharZero(R/I)$$$

Lean4

/-- Not mixed characteristic implies equal characteristic. -/
theorem of_not_mixedCharZero [CharZero R] (h : ∀ p > 0, ¬MixedCharZero R p) : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I) :=
  by
  intro I hI_ne_top
  suffices CharP (R ⧸ I) 0 from CharP.charP_to_charZero _
  cases CharP.exists (R ⧸ I) with
  | intro p hp =>
    cases p with
    | zero => exact hp
    | succ p =>
      have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
      exact absurd h_mixed (h p.succ p.succ_pos)

Похожие утверждения