iff_not_mixedCharZero — Mathlib

English

Equal characteristic zero is equivalent to not having any mixed characteristic.

Русский

Равная характеристика нулю эквивалентна отсутствию смешанной характеристики.

LaTeX

$$$[CharZero R] \\iff (\\forall p>0, \\neg MixedCharZero(R,p))$$$

Lean4

/-- A ring of characteristic zero has equal characteristic iff it does not
have mixed characteristic for any `p`.
-/
theorem iff_not_mixedCharZero [CharZero R] : (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)) ↔ ∀ p > 0, ¬MixedCharZero R p :=
  ⟨to_not_mixedCharZero R, of_not_mixedCharZero R⟩

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