dividedPowers — Mathlib

English

For a commutative ring A of prime characteristic p, with I^p = 0, there is a divided powers structure on I given by IsNilpotent.dividedPowers.

Русский

Для коммутативного кольца A с характеристикой p, и при I^p = 0, существует структура разделённых степеней на I, задаваемая IsNilpotent.dividedPowers.

LaTeX

$$$CharP\ A\ p \land I^p = 0 \Rightarrow DividedPowers\ CharP.dividedPowers I$$$

Lean4

/-- If `A` is a commutative ring of prime characteristic `p` and `I` is an ideal such that
  `I^p = 0`, then `I` admits a divided power structure. -/
noncomputable def dividedPowers : DividedPowers I :=
  IsNilpotent.dividedPowers ((CharP.cast_eq_zero A p) ▸ IsNilpotent.zero) hIp

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