mathlib

398f60f6 - feat(linear_algebra): the direct sum of a submodule quotient is the quotient of the direct sum (#17069)

feat(linear_algebra): the direct sum of a submodule quotient is the quotient of the direct sum (#17069) This defines the linear equivalence `submodule.quotient_pi` which allows us to interchange taking the direct sum and taking the quotient. This result is useful for defining the ideal norm. Co-Authored-By: Alex J. Best <alex.j.best@gmail.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>