map_isMaximal_of_equiv — Mathlib

English

A ring isomorphism sends a maximal ideal to a maximal ideal.

Русский

Кольцевый изоморфизм отправляет максимальный идеал в максимальный.

LaTeX

$$map_isMaximal_of_equiv : (map e p).IsMaximal$$

Lean4

/-- A ring isomorphism sends a maximal ideal to a maximal ideal. -/
instance map_isMaximal_of_equiv {E : Type*} [EquivLike E R S] [RingEquivClass E R S] (e : E) {p : Ideal R}
    [hp : p.IsMaximal] : (map e p).IsMaximal :=
  hp.map_bijective e (EquivLike.bijective e)

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