mathlib3

e5ba338e - fix(algebra/direct_sum): change `ring_hom_ext` to not duplicate `ring_hom_ext'` (#10640)

fix(algebra/direct_sum): change `ring_hom_ext` to not duplicate `ring_hom_ext'` (#10640) These two lemmas differed only in the explicitness of their binders. The statement of the unprimed version has been changed to be fully applied. This also renames `alg_hom_ext` to `alg_hom_ext'` to make way for the fully applied version. This is consistent with `direct_sum.add_hom_ext` vs `direct_sum.add_hom_ext'`.