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
.