English
If J is another ideal with divided powers, and a ∈ I·J, then dpow_n(a) computed with respect to I equals that computed with respect to J.
Русский
Если J — другой идеал с делёнными степенями, и a ∈ I·J, то dpow_n(a) относительно I совпадает с dpow_n(a) относительно J.
LaTeX
$$$hI.dpow\\, n\\ a = hJ.dpow\\, n\\ a \\quad\\text{for } a \\in I \\cdot J$$$
Lean4
/-- If J is another ideal of A with divided powers,
then the divided powers of I and J coincide on I • J
[Berthelot-1974], 1.6.1 (ii) -/
theorem coincide_on_smul {J : Ideal A} (hJ : DividedPowers J) {n : ℕ} (ha : a ∈ I • J) : hI.dpow n a = hJ.dpow n a := by
induction ha using Submodule.smul_induction_on' generalizing n with
| smul a ha b
hb =>
rw [Algebra.id.smul_eq_mul, hJ.dpow_mul hb, mul_comm a b, hI.dpow_mul ha, ← hJ.factorial_mul_dpow_eq_pow hb, ←
hI.factorial_mul_dpow_eq_pow ha]
ring
| add x hx y hy hx'
hy' =>
rw [hI.dpow_add (mul_le_right hx) (mul_le_right hy), hJ.dpow_add (mul_le_left hx) (mul_le_left hy)]
apply sum_congr rfl
intro k _
rw [hx', hy']
