isSubDPIdeal_map — Mathlib

English

The image of a divided power morphism from I to J is a sub-dp-ideal of J.

Русский

Образ dp-морфизма из I в J является под dp-идеалом над J.

LaTeX

$$IsSubDPIdeal hJ (Ideal.map f I)$$

Lean4

/-- The image of a divided power morphism from `I` to `J` is a sub-dp-ideal of `J`. -/
theorem isSubDPIdeal_map {f : A →+* B} (hf : IsDPMorphism hI hJ f) : IsSubDPIdeal hJ (Ideal.map f I) :=
  isSubDPIdeal_map_of_isSubDPIdeal hf (IsSubDPIdeal.self hI)

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