English
There is a construction DividedPowers OfInvertibleFactorial, giving a divided power structure on I provided (n-1)! is a unit and I^n = 0.
Русский
Существует конструкция DividedPowers OfInvertibleFactorial, задающая структуру разделённых степеней на идеал I при условии, что (n-1)! — единичный элемент и I^n = 0.
LaTeX
$$$\text{dividedPowers}:= \text{OfInvertibleFactorial.dividedPowers} (n)\left(IsUnit ((n-1)!:A)\right) (I^n=0)$$$
Lean4
/-- If `(n-1)!` is invertible in `A` and `I^n = 0`, then `I` admits a divided power structure.
Proposition 1.2.7 of [B74], part (ii). -/
noncomputable def dividedPowers {n : ℕ} (hn_fac : IsUnit ((n - 1).factorial : A)) (hnI : I ^ n = 0) : DividedPowers I
where
dpow := dpow I
dpow_null hx := dpow_null hx
dpow_zero hx := dpow_zero hx
dpow_one hx := dpow_one hx
dpow_mem hn hx := dpow_mem hn hx
dpow_add hx hy := dpow_add hn_fac hnI hx hy
dpow_mul := dpow_mul
mul_dpow hx := mul_dpow hn_fac hnI hx
dpow_comp hk hx := dpow_comp hn_fac hnI hk hx
