dividedPowers_unique — Mathlib

English

Given hI and IsSubDPIdeal data, the equality DividedPowers.Quotient.dividedPowers is the unique DP-structure on the quotient.

Русский

При заданном hI и IsSubDPIdeal единственная DP-структура на факторе задаётся DividedPowers.Quotient.dividedPowers.

LaTeX

$$$DividedPowers.Quotient.dividedPowers\\_unique(hI,hIJ)\\Rightarrow hquot = DividedPowers.Quotient.dividedPowers(hI,hIJ)$$$

Lean4

theorem dividedPowers_unique (hquot : DividedPowers (I.map (Ideal.Quotient.mk J)))
    (hm : DividedPowers.IsDPMorphism hI hquot (Ideal.Quotient.mk J)) : hquot = dividedPowers hI hIJ :=
  DividedPowers.Quotient.OfSurjective.dividedPowers_unique hI Ideal.Quotient.mk_surjective (refl _)
    (isSubDPIdeal_aux hI hIJ) hquot hm

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