Commit 2025-08-16 00:47 a655f149

View on Github →

chore(Topology/Compactification): deprecate duplicate ultrafilter_pure_injective (#28436)

Estimated changes

Modified Mathlib/Topology/Compactification/StoneCech.lean

deleted theorem ultrafilter_pure_injective