coe_ideal_map — Mathlib

English

The image of an ideal under an algebra hom equals the image under its underlying ring hom.

Русский

Образ идеала под алгебраическим отображением совпадает с образoм под соответствующим кольцевым отображением.

LaTeX

$$$$ \\operatorname{Ideal.map} f I = \\operatorname{Ideal.map} \\bigl( f:A\\to^+*B \\bigr) I. $$$$

Lean4

theorem coe_ideal_map (I : Ideal A) : Ideal.map f I = Ideal.map (f : A →+* B) I :=
  rfl

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