isEmpty_algebraRat_iff_mixedCharZero

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

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