dividedPowers — Mathlib

English

If I^2 = 0, then I carries a divided power structure obtained from OfInvertibleFactorial.

Русский

Если I^2 = 0, то I имеет структуру разделённых степеней, получаемую из OfInvertibleFactorial.

LaTeX

$$$I^2 = 0 \Rightarrow DividedPowers\ OfSquareZero \dividedPowers \ I$$$

Lean4

/-- If `I^2 = 0`, then `I` admits a divided power structure. -/
noncomputable def dividedPowers : DividedPowers I :=
  OfInvertibleFactorial.dividedPowers (by norm_num) hI2

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