Commit 2021-12-08 05:53 e5ba338e

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'.