fact: Definition ideal_sum_ind {R : CRing} (I J : Ideal R) (P : forall x, ideal_sum I J x -> Type) (P_I_in : forall x y, P x (tr (sgt_in (inl y)))) (P_J_in : forall x y, P x (tr (sgt_in (inr y)))) (P_unit : P mon_unit (tr sgt_unit)) (P_op : forall x y h k, P x (tr h) -> P y (tr k) -> P (x - y) (tr (sgt_op h k))) `{forall x y, IsHProp (P x y)} : forall x (p : ideal_sum I J x), P x p := subgroup_product_ind I J P P_I_in P_J_in P_unit P_op.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups