isField_of_isIntegral_of_isField — Mathlib

English

If the integral extension R → S is injective and S is a field, then R is a field.

Русский

Если интегральное расширение R → S инъективно и S является полем, то R есть поле.

LaTeX

$$$f:\\,R\\to S \\text{ integral} \\wedge \\text{Injective}(f) \\wedge \\text{IsField}(S) \\Rightarrow \\text{IsField}(R)$$$

Lean4

/-- If the integral extension `R → S` is injective, and `S` is a field, then `R` is also a field. -/
theorem isField_of_isIntegral_of_isField (hRS : Function.Injective (algebraMap R S)) (hS : IsField S) : IsField R :=
  have := (faithfulSMul_iff_algebraMap_injective R S).mpr hRS
  IsLocalHom.isField hRS hS

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