nonempty_algebraRat_iff — Mathlib

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

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