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: port Topology.Algebra.Order.Field #2626
Conversation
596e6d5
to
1c027f0
Compare
ada1055
to
1a36d9b
Compare
This will still need a forward-port PR to update the sha |
@@ -77,6 +77,8 @@ protected def symm (h : α ≃ₜ β) : β ≃ₜ α where | |||
toEquiv := h.toEquiv.symm | |||
#align homeomorph.symm Homeomorph.symm | |||
|
|||
@[simp] theorem symm_symm (h : α ≃ₜ β) : h.symm.symm = h := rfl |
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.
This will need an #align
once the backport goes through. It might be sensible to add it now so we don't forget.
4ebfa6b
to
799074e
Compare
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
799074e
to
b37e208
Compare
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.
Thanks 🎉
bors merge
I made substantial changes to the proofs. To avoid backporting most of them, in leanprover-community/mathlib#18552 I add `private` to lemmas that are deleted in this PR. Also, I backport `Homeomorph.symm_symm` in leanprover-community/mathlib#18551
Pull request successfully merged into master. Build succeeded:
|
I made substantial changes to the proofs. To avoid backporting most of them, in leanprover-community/mathlib#18552 I add
private
to lemmas that are deleted in this PR. Also, I backportHomeomorph.symm_symm
in leanprover-community/mathlib#18551