isField_iff_isField — Mathlib

English

For an integral extension R → S with injection, IsField R is equivalent to IsField S (for domain S).

Русский

Для интегрального расширения R → S с инъекцией: R является полем тогда и только тогда, когда S является полем (при условии, что S домен).

LaTeX

$$$[IsDomain S] \\Rightarrow (\\text{Injective}(algebraMap R S) \\Rightarrow IsField R \\leftrightarrow IsField S)$$$

Lean4

theorem isField_iff_isField [IsDomain S] (hRS : Function.Injective (algebraMap R S)) : IsField R ↔ IsField S :=
  ⟨isField_of_isIntegral_of_isField', isField_of_isIntegral_of_isField hRS⟩

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