maximal_ideal_iff_isField_quotient

English

An ideal is maximal if and only if the quotient is a field.

Русский

Идеал максимален тогда и только тогда, когда фактор-кольцо является полем.

LaTeX

$$$I.IsMaximal \iff IsField (R / I)$$$

Lean4

/-- The quotient of a ring by an ideal is a field iff the ideal is maximal. -/
theorem maximal_ideal_iff_isField_quotient {R} [CommRing R] (I : Ideal R) : I.IsMaximal ↔ IsField (R ⧸ I) :=
  ⟨fun h =>
    let _i := @Quotient.field _ _ I h
    Field.toIsField _,
    maximal_of_isField _⟩

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