# Commit 2024-10-29 16:55 07a7b10f

View on Github →chore(LinearAlgebra): split `Quotient.lean`

into `Defs`

and `Basic`

(#18384)
This PR rearranges the definitions of quotient modules as follows:

`LinearAlgebra/QuotientPi.lean`

is renamed`LinearAlgebra/Quotient/Pi.lean`

`LinearAlgebra/Quotient.lean`

is split into`LinearAlgebra/Quotient/Defs.lean`

(with the definition and module structure of the quotient module)`LinearAlgebra/Quotient/Basic.lean`

(with some basic maps for the quotient)