mk' — Mathlib

English

From a ring homomorphism f known to be a DividedPowers morphism, we obtain a DPMorphism structure on (I, J).

Русский

Из гомоморфизма кольца f, удовлетворяющего условию делённых степеней, получаем структуру DPMorphism на (I, J).

LaTeX

$$def mk' {f : A →+* B} (hf : IsDPMorphism hI hJ f) : DPMorphism hI hJ$$

Lean4

/-- A constructor for `DPMorphism` from a ring homomorphism `f : A →+* B` satisfying
  `IsDPMorphism hI hJ f`. -/
def mk' {f : A →+* B} (hf : IsDPMorphism hI hJ f) : DPMorphism hI hJ :=
  ⟨f, hf.1, hf.2⟩

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