Lean4
/-- If `J` is an ideal of `A`, then `I⬝J` is a sub-dp-ideal of `I`.
See [P. Berthelot, *Cohomologie cristalline des schémas de caractéristique $p$ > 0*,
(Proposition 1.6.1 (i))][Berthelot-1974] -/
def prod (J : Ideal A) : SubDPIdeal hI where
carrier := I • J
isSubideal := mul_le_right
dpow_mem m hm x
hx := by
induction hx using Submodule.smul_induction_on' generalizing m with
| smul a ha b hb =>
rw [Algebra.id.smul_eq_mul, smul_eq_mul, mul_comm a b, hI.dpow_mul ha, mul_comm]
exact Submodule.mul_mem_mul (J.pow_mem_of_mem hb m (zero_lt_iff.mpr hm)) (hI.dpow_mem hm ha)
| add x hx y hy hx' hy' =>
rw [hI.dpow_add' (mul_le_right hx) (mul_le_right hy)]
apply Submodule.sum_mem (I • J)
intro k _
by_cases hk0 : k = 0
· exact hk0 ▸ mul_mem_left (I • J) _ (hy' _ hm)
· exact mul_mem_right _ (I • J) (hx' k hk0)
