mathlib

cb2777cb - feat(ring_theory/graded_algebra): projection map of graded algebra (#10116)

feat(ring_theory/graded_algebra): projection map of graded algebra (#10116) This pr defines and proves some property about `graded_algebra.proj : A →ₗ[R] A` Co-authored-by: jjaassoonn <jujian.zhang1998@out.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>