# Commit 2024-10-29 15:17 90ab0257

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

(#18383)
This PR splits off various definitions and results from `RingTheory/Ideal/Basic.lean`

:

`Ideal`

goes to`Ideal/Defs.lean`

- results on
`⊥`

,`⊤`

,`⊔`

,`⊓`

go to`Ideal/Lattice.lean`

`Ideal.IsPrime`

goes to`Ideal/Prime.lean`

`IsPrincipalIdealDomain`

and`Ideal.span`

go to`Ideal/Span.lean`

`Ideal.IsMaximal`

goes to`Ideal/Maximal.lean`