dividedPowers — Mathlib

English

The Infimum construction in the quotient setting yields a legitimate DividedPowers on the image ideal, given IsSubDPIdeal hypotheses.

Русский

Полученная конструкцияInf в факторной ситуации образует законную DP-структуру на образующемидеале при гипотезе IsSubDPIdeal.

LaTeX

$$$DividedPowers.Quotient.inf$ (условие) $$

Lean4

/-- When `I ⊓ J` is a sub-dp-ideal of `I`, this is the divided power structure on the ideal
 `I(A⧸J)` of the quotient. -/
noncomputable def dividedPowers : DividedPowers (I.map (Ideal.Quotient.mk J)) :=
  DividedPowers.Quotient.OfSurjective.dividedPowers hI Ideal.Quotient.mk_surjective (refl _) (isSubDPIdeal_aux hI hIJ)

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