nonempty_field — Mathlib

English

Any infinite type admits a field structure; i.e., there exists a field with that underlying set.

Русский

Любой бесконечный тип можно наделить структурами поля; существует поле с данным множеством.

LaTeX

$$There exists a field structure on any infinite set: ∃ Field α with |α| infinite.$$

Lean4

/-- Any infinite type can be endowed a field structure. -/
theorem nonempty_field {α : Type u} [Infinite α] : Nonempty (Field α) :=
  by
  suffices #α = #(FractionRing (MvPolynomial α <| ULift.{u} ℚ)) from (Cardinal.eq.1 this).map (·.field)
  simp

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