English
For a divided powers structure on I in a ℚ-algebra, there is no other such structure; it is unique.
Русский
Для структуры разделённых степеней на I в ℚ-алгебре такая структура единственна.
LaTeX
$$$\text{dividedPowers}$ unique: \; hI = dividedPowers I$$$
Lean4
/-- If `I` is an ideal in a `ℚ`-algebra `A`, then `I` admits a unique divided power structure,
given by `dpow n x = x ^ n / n!`. -/
noncomputable def dividedPowers : DividedPowers I
where
dpow := dpow I
dpow_null hx := OfInvertibleFactorial.dpow_null hx
dpow_zero hx := OfInvertibleFactorial.dpow_zero hx
dpow_one hx := OfInvertibleFactorial.dpow_one hx
dpow_mem hn hx := OfInvertibleFactorial.dpow_mem hn hx
dpow_add {n} _ _ hx
hy := OfInvertibleFactorial.dpow_add_of_lt (IsUnit.natCast_factorial_of_algebra ℚ _) (n.lt_succ_self) hx hy
dpow_mul hx := OfInvertibleFactorial.dpow_mul hx
mul_dpow {m} k _
hx := OfInvertibleFactorial.dpow_mul_of_add_lt (IsUnit.natCast_factorial_of_algebra ℚ _) (m + k).lt_succ_self hx
dpow_comp hk
hx := OfInvertibleFactorial.dpow_comp_of_mul_lt (IsUnit.natCast_factorial_of_algebra ℚ _) hk (lt_add_one _) hx
