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] - refactor(linear_algebra, analysis/inner_product_space): use ⊤ ≤
instead of = ⊤
in bases constructors
#15697
Conversation
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.
I like this change a lot! Since it touches widely-used files in linear algebra, I won't take the initiative to merge it immediately.
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.
LGTM. I'll bors it if the Zulip thread is still positive after it's been up for a couple of hours.
The consensus is positive, so: bors merge |
…tead of `= ⊤` in bases constructors (#15697) All the existing proof just need a `.ge` to be fixed, and this allows to remove a lot of `rw [eq_top_iff]`, and it sticks with the convention of having weakest forms in assumptions and stronger forms in conclusion. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60.E2.8A.A4.20.E2.89.A4.20span.60.20in.20basis.20constructors
Build failed: |
Could you please merge master and fix the issues? bors d+ |
✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…tead of `= ⊤` in bases constructors (#15697) All the existing proof just need a `.ge` to be fixed, and this allows to remove a lot of `rw [eq_top_iff]`, and it sticks with the convention of having weakest forms in assumptions and stronger forms in conclusion. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60.E2.8A.A4.20.E2.89.A4.20span.60.20in.20basis.20constructors
Pull request successfully merged into master. Build succeeded: |
⊤ ≤
instead of = ⊤
in bases constructors⊤ ≤
instead of = ⊤
in bases constructors
…tead of `= ⊤` in bases constructors (leanprover-community#15697) All the existing proof just need a `.ge` to be fixed, and this allows to remove a lot of `rw [eq_top_iff]`, and it sticks with the convention of having weakest forms in assumptions and stronger forms in conclusion. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60.E2.8A.A4.20.E2.89.A4.20span.60.20in.20basis.20constructors
…tead of `= ⊤` in bases constructors (#15697) All the existing proof just need a `.ge` to be fixed, and this allows to remove a lot of `rw [eq_top_iff]`, and it sticks with the convention of having weakest forms in assumptions and stronger forms in conclusion. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60.E2.8A.A4.20.E2.89.A4.20span.60.20in.20basis.20constructors
…tead of `= ⊤` in bases constructors (#15697) All the existing proof just need a `.ge` to be fixed, and this allows to remove a lot of `rw [eq_top_iff]`, and it sticks with the convention of having weakest forms in assumptions and stronger forms in conclusion. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60.E2.8A.A4.20.E2.89.A4.20span.60.20in.20basis.20constructors
All the existing proof just need a
.ge
to be fixed, and this allows to remove a lot ofrw [eq_top_iff]
, and it sticks with the convention of having weakest forms in assumptions and stronger forms in conclusion.Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60.E2.8A.A4.20.E2.89.A4.20span.60.20in.20basis.20constructors