basic): golf `graded_ring.proj_zero_ring_hom` (#16081)

Commit

3 years ago

chore(ring_theory/graded_algebra/basic): golf `graded_ring.proj_zero_ring_hom` (#16081) use `direct_sum.decomposition.induction_on` instead of manually writing out inductions

Author

jjaassoonn

Parents

ce566b31

mathlib3 35f49417 - chore(ring_theory/graded_algebra/basic): golf `graded_ring.proj_zero_ring_hom` (#16081)

mathlib3
35f49417 - chore(ring_theory/graded_algebra/basic): golf `graded_ring.proj_zero_ring_hom` (#16081)