English
In a commutative ring of prime characteristic p, the divided power structure on I is given by IsNilpotent.dividedPowers.
Русский
В коммутативном кольце с простой характеристикой p структура разделённых степеней на I задаётся через IsNilpotent.dividedPowers.
LaTeX
$$DividedPowers.CharP.dividedPowers A p hIp$$
Lean4
/-- If `I` is an ideal in a `ℚ`-algebra `A`, then the divided power structure on `I` given by
`dpow n x = x ^ n / n!` is the only possible one. -/
theorem dpow_eq_inv_fact_smul (hI : DividedPowers I) {n : ℕ} {x : R} (hx : x ∈ I) :
hI.dpow n x = (inverse (n.factorial : ℚ)) • x ^ n :=
by
rw [inverse_eq_inv', ← factorial_mul_dpow_eq_pow hI hx, ← smul_eq_mul, ← smul_assoc]
nth_rewrite 1 [← one_smul R (hI.dpow n x)]
congr
have aux : ((n !) : R) = (n ! : ℚ) • (1 : R) := by rw [cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
rw [aux, ← mul_smul]
suffices (n ! : ℚ)⁻¹ * (n !) = 1 by rw [this, one_smul]
apply Rat.inv_mul_cancel
rw [← cast_zero, ne_eq]
simp [factorial_ne_zero]
