Intrinsic and module-skeleton radical-square definitions agree

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.intrinsic_radicalSquare_eq {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (S : IndecomposableSkeleton R ι) (x y : ι) : (CategoricalRadical.homIdeal ⋆ᵢ CategoricalRadical.homIdeal).hom (S.obj x) (S.obj y) = S.radicalSquareHomAddSubgroup x y

The intrinsic product ideal has the same Hom subgroup as the existing arbitrary-middle radical-square factorization predicate.