isDPMorphism — Mathlib

English

Given a DividedPowers morphism f as a DPMorphism, its underlying ring homomorphism is an IsDPMorphism.

Русский

Дано отображение делённых степеней f как DPMorphism, тогда соответствующее кольцевое отображение удовлетворяет условию IsDPMorphism.

LaTeX

$$isDPMorphism (f : DPMorphism hI hJ) : IsDPMorphism hI hJ f.toRingHom$$

Lean4

theorem isDPMorphism (f : DPMorphism hI hJ) : IsDPMorphism hI hJ f.toRingHom :=
  ⟨f.ideal_comp, f.dpow_comp⟩

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