mathlib3

6f23973a - feat(ring_theory/graded_algebra/basic): add a helper for construction from an alg hom (#11541)

feat(ring_theory/graded_algebra/basic): add a helper for construction from an alg hom (#11541) Most graded algebras are already equipped with some kind of universal property which gives an easy way to build such an `alg_hom`. This lemma makes it easier to discharge the associated proof obligations to show that this alg hom forms a decomposition. This also relaxes a `ring` argument to `semiring`.