Commit 2025-05-02 03:05 3703f458
View on Github →refactor(FieldTheory/KrullTopology): clean up KrullTopology.lean (#22971)
Clean up KrullTopology.lean by moving some lemmas to their appropriate locations in earlier files.
Also move some lemmas from IntermediateField/Adjoin/Defs.lean to IntermediateField/Basic.lean since they are used in the proofs of new theorems in IntermediateField/Algebraic.lean.