-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(topology/algebra): Inf and inducing preserve compatibility with algebraic structure #11720
Conversation
…ity/mathlib into AD_top_lattice_algebra
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Without investigating very deeply, I think in earlier commits you had two problems:
- You were putting multiple
topological_group
instances on the same type, which is never a good idea - I think type-class inference cannot deal with hypotheses of the form
[∀ t ∈ ts, @topological_group G t _]
. Note that this depends on a hypothesis(H : t ∈ ts)
which cannot be figured out itself by type-class inference.
These lemmas are fine, and can locally be used with haveI/letI
.
One minor comment, otherwise, LGTM
bors d+
✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…algebraic structure (#11720) This partly duplicates @mariainesdff 's work on group topologies, but I'm using an unbundled approach which avoids defining a new `X_topology` structure for each interesting X.
Pull request successfully merged into master. Build succeeded: |
This partly duplicates @mariainesdff 's work on group topologies, but I'm using an unbundled approach which avoids defining a new
X_topology
structure for each interesting X.