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/*): add lemma linear_independent.finite_of_is_noetherian
#14714
Conversation
…etherian` This replaces `fintype_of_is_noetherian_linear_independent` which gave the same conclusion except demanded `strong_rank_condition R` instead of just `nontrivial R`. Also some other minor gaps filled.
f05ad01
to
d7702c9
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.
LGTM. I left two tiny comments.
src/order/sup_indep.lean
Outdated
refine (supr_mono $ λ i, _).trans (supr_comp_le _ f), | ||
exact supr_const_mono hf.ne, | ||
end | ||
|
||
lemma independent.comp' |
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.
The names independent.comp
and independent.comp'
are not great. It's not easy to understand from names that composition is not on the same side. Maybe independent.comp_inj
and independent.of_comp_surj
or something? It's not really clearer...
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 agree but I'm not sure about comp_inj
and of_comp_surj
either.
…ndent_span_singleton` Suggestion of CR
…e.well_founded.finite_of_independent`
Thanks bors r+ |
…etherian` (#14714) This replaces `fintype_of_is_noetherian_linear_independent` which gave the same conclusion except demanded `strong_rank_condition R` instead of just `nontrivial R`. Also some other minor gaps filled.
Build failed (retrying...): |
…etherian` (#14714) This replaces `fintype_of_is_noetherian_linear_independent` which gave the same conclusion except demanded `strong_rank_condition R` instead of just `nontrivial R`. Also some other minor gaps filled.
Pull request successfully merged into master. Build succeeded: |
linear_independent.finite_of_is_noetherian
linear_independent.finite_of_is_noetherian
This replaces
fintype_of_is_noetherian_linear_independent
which gave the sameconclusion except demanded
strong_rank_condition R
instead of justnontrivial R
.Also some other minor gaps filled.