surjective_iff_isField — Mathlib

English

If R is a domain, then the surjectivity of the algebra map R → K is equivalent to R being a field.

Русский

Если R — область, то сюръективность алгебраической карты R → K эквивалентна тому, что R — поле.

LaTeX

$$Surjective(algebraMap R K) \iff IsField(R)$$

Lean4

theorem surjective_iff_isField [IsDomain R] : Function.Surjective (algebraMap R K) ↔ IsField R
    where
  mp
    h :=
    (RingEquiv.ofBijective (algebraMap R K) ⟨IsFractionRing.injective R K, h⟩).toMulEquiv.isField
      (IsFractionRing.toField R).toIsField
  mpr
    h :=
    letI := h.toField
    (IsLocalization.atUnits R _ (S := K) (fun _ hx ↦ Ne.isUnit (mem_nonZeroDivisors_iff_ne_zero.mp hx))).surjective

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