English
A ring has a ℚ-algebra iff it has equal characteristic zero.
Русский
Кольцо имеет ℚ-алгебру тогда и только тогда, когда характеристика кольца равна нулю.
LaTeX
$$$\\text{Nonempty}(\\text{Algebra }\\mathbb{Q} \\; R) \\iff \\forall I, I \\neq \\top \\to CharZero(R/I)$$$
Lean4
/-- A ring is a `ℚ`-algebra iff it has equal characteristic zero. -/
theorem nonempty_algebraRat_iff : Nonempty (Algebra ℚ R) ↔ ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I) :=
by
constructor
· intro h_alg
haveI h_alg' : Algebra ℚ R := h_alg.some
apply of_algebraRat
· intro h
apply Nonempty.intro
exact algebraRat h