to_not_mixedCharZero — Mathlib

English

If CharZero holds in every quotient of R, then R has not mixed characteristic.

Русский

Если CharZero держится во всех фактор-колцах R, тогда R не имеет смешанной характеристики.

LaTeX

$$$\\forall p>0, \\neg MixedCharZero(R,p)$$$

Lean4

/-- Equal characteristic implies not mixed characteristic. -/
theorem to_not_mixedCharZero (h : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)) : ∀ p > 0, ¬MixedCharZero R p :=
  by
  intro p p_pos
  by_contra hp_mixedChar
  rcases hp_mixedChar.charP_quotient with ⟨I, hI_ne_top, hI_p⟩
  replace hI_zero : CharP (R ⧸ I) 0 := @CharP.ofCharZero _ _ (h I hI_ne_top)
  exact absurd (CharP.eq (R ⧸ I) hI_p hI_zero) (ne_of_gt p_pos)

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