Commit 2023-09-06 11:21 a0109979

View on Github →

feat: The forgetful functor on Stonean has a left adjoint given by Stone-Cech compactification (#6826)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/Stonean/Adjunctions.lean

added theorem Stonean.mono_iff_injective

added def Stonean.stoneCechObj