Lean4
/-- The divided power structure on a sub-dp-ideal. -/
def dividedPowers {J : Ideal A} (hJ : IsSubDPIdeal hI J) [∀ x, Decidable (x ∈ J)] : DividedPowers J
where
dpow n x := if x ∈ J then hI.dpow n x else 0
dpow_null hx := by simp [if_neg hx]
dpow_zero hx := by simp [if_pos hx, hI.dpow_zero (hJ.isSubideal hx)]
dpow_one hx := by simp [if_pos hx, hI.dpow_one (hJ.isSubideal hx)]
dpow_mem hn hx := by simp [if_pos hx, hJ.dpow_mem _ hn hx]
dpow_add hx
hy := by
simp_rw [if_pos hx, if_pos hy, if_pos (Ideal.add_mem J hx hy), hI.dpow_add (hJ.isSubideal hx) (hJ.isSubideal hy)]
dpow_mul hx := by simp [if_pos hx, if_pos (mul_mem_left J _ hx), hI.dpow_mul (hJ.isSubideal hx)]
mul_dpow hx := by simp [if_pos hx, hI.mul_dpow (hJ.isSubideal hx)]
dpow_comp hn hx := by simp [if_pos hx, if_pos (hJ.dpow_mem _ hn hx), hI.dpow_comp hn (hJ.isSubideal hx)]
