mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

feat(topology/algebra/module/basic): a hyperplane is either closed or dense

Open ADedecker opened this issue 3 years ago • 1 comments
trafficstars


  • [x] depends on: #16786

Open in Gitpod

ADedecker avatar Oct 03 '22 16:10 ADedecker

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16786~~ By Dependent Issues (🤖). Happy coding!

:v: ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Oct 14 '22 13:10 bors[bot]

bors r+

ADedecker avatar Oct 15 '22 08:10 ADedecker

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 15 '22 13:10 bors[bot]