comap_isMaximal_of_equiv — Mathlib

English

The pullback of a maximal ideal under an isomorphism is maximal.

Русский

Обратное отображение максимального идеала через изоморфизм сохраняет максимальность.

LaTeX

$$comap_isMaximal_of_equiv : IsMaximal (comap e p)$$

Lean4

/-- The pullback of a maximal ideal under a ring isomorphism is a maximal ideal. -/
instance comap_isMaximal_of_equiv {E : Type*} [EquivLike E R S] [RingEquivClass E R S] (e : E) {p : Ideal S}
    [hp : p.IsMaximal] : (comap e p).IsMaximal :=
  hp.comap_bijective e (EquivLike.bijective e)

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