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.

Estimated changes