Commit 2025-06-23 15:53 464bf246
View on Github →feat: unit space of a (locally) compact T1 monoid is (locally) compact (#26153) This PR continues the work from #25235. Original PR: https://github.com/leanprover-community/mathlib4/pull/25235
feat: unit space of a (locally) compact T1 monoid is (locally) compact (#26153) This PR continues the work from #25235. Original PR: https://github.com/leanprover-community/mathlib4/pull/25235