English
The existence of a ℚ-algebra structure is equivalent to the existence of some p with MixedCharZero.
Русский
Существование ℚ-алгебра эквивалентно существованию какого-то p с MixedCharZero.
LaTeX
$$$IsEmpty(\\text{Algebra }\\mathbb{Q} R) \\iff \\exists p>0, MixedCharZero(R,p)$$$
Lean4
/-- A ring of characteristic zero is not a `ℚ`-algebra iff it has mixed characteristic for some `p`.
-/
theorem isEmpty_algebraRat_iff_mixedCharZero [CharZero R] : IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p :=
by
rw [← not_iff_not]
push_neg
rw [← EqualCharZero.iff_not_mixedCharZero]
apply EqualCharZero.nonempty_algebraRat_iff