Commit 2025-01-10 04:48 a8fc4672

View on Github →

chore: reduce Topology->Order imports by moving content (#20627)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Category/Frm.lean

deleted def topCatOpToFrm

Modified Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean

Created Mathlib/Topology/Category/CompHaus/Frm.lean

added def topCatOpToFrm

Modified Mathlib/Topology/Category/Locale.lean