isSimpleRing_iff_isField — Mathlib

English

A commutative ring A is simple if and only if A is a field.

Русский

Коммутативное кольцо A простое тогда и только тогда, когда A — поле.

LaTeX

$$For a commutative ring A, IsSimpleRing A ↔ IsField A.$$

Lean4

theorem isSimpleRing_iff_isField (A : Type*) [CommRing A] : IsSimpleRing A ↔ IsField A :=
  ⟨fun _ ↦
    Subring.topEquiv.symm.toMulEquiv.isField <| by rw [← Subring.center_eq_top A]; exact IsSimpleRing.isField_center A,
    fun h ↦
    letI := h.toField;
    inferInstance⟩

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