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(linear_algebra/basic): some lemmas about span and restrict_scalars #10167
Conversation
eric-wieser
commented
Nov 4, 2021
00c986b
to
20a4181
Compare
@@ -800,9 +801,15 @@ span_le.2 $ subset.trans h subset_span | |||
lemma span_eq_of_le (h₁ : s ⊆ p) (h₂ : p ≤ span R s) : span R s = p := | |||
le_antisymm (span_le.2 h₁) h₂ | |||
|
|||
@[simp] lemma span_eq : span R (p : set M) = p := | |||
lemma span_eq : span R (p : set M) = p := |
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'm quite surprised to see simp
being removed here. Is there an easy explanation of why we shouldn't keep it?
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.
Yes, the linter complains! This is now proved via the new lemma
I'd like to understand the reason for dropping the bors d+ |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge See above, the linter forced my hand. |
Pull request successfully merged into master. Build succeeded: |