isField_of_isIntegral_of_isField'

English

If a commutative domain is integral over a field, then it is a field.

Русский

Если коммутативный домен интегральный над полем, то он является полем.

LaTeX

$$$\\text{IsField}(S) \\text{ if } [\\text{CommRing } R], [\\text{IsDomain } S], [\\text{Algebra } R S], [\\text{Algebra.IsIntegral } R S].$$$

Lean4

/-- A commutative domain that is an integral algebra over a field is a field. -/
theorem isField_of_isIntegral_of_isField' [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] [Algebra.IsIntegral R S]
    (hR : IsField R) : IsField S where
  exists_pair_ne := ⟨0, 1, zero_ne_one⟩
  mul_comm := mul_comm
  mul_inv_cancel {x}
    hx := by
    letI := hR.toField
    obtain ⟨y, rfl⟩ := (Algebra.IsIntegral.isIntegral (R := R) x).isUnit hx
    exact ⟨y.inv, y.val_inv⟩

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