# Commit 2024-10-30 08:00 abfa430b

View on Github →chore(RingTheory/Ideal): split `Quotient.lean`

into `Defs`

and `Basic`

(#18393)
This PR renames and splits files involved in the ideal quotient.
Changes:

`RingTheory/Ideal/Quotient.lean`

is split into`RingTheory/Ideal/Quotient/Defs.lean`

(definition of ideal quotient and ring structure)

`RingTheory/Ideal/Quotient/Basic.lean`

(further results)`RingTheory/QuotientNilpotent.lean`

is renamed to`RingTheory/Ideal/Quotient/Nilpotent.lean`

`RingTheory/QuotientNoetherian.lean`

is renamed to`Mathlib/RingTheory/Ideal/Quotient/Noetherian.lean`

`RingTheory/Ideal/QuotientOperations.lean`

is renamed to`Mathlib/RingTheory/Ideal/Quotient/Operations.lean`