-
Notifications
You must be signed in to change notification settings - Fork 298
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/free_module/ideal_quotient): add ideal.finrank_quotient_eq_sum #19084
Conversation
Part of the auxiliary file in #18000 |
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, LGTM!
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Thanks! maintainer merge |
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
lemma ideal.finrank_quotient_eq_sum [nontrivial F] | ||
[∀ i, module.free F (R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R))] | ||
[∀ i, module.finite F (R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R))] : | ||
finite_dimensional.finrank F (S ⧸ I) | ||
= ∑ i, finite_dimensional.finrank F (R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R)) := | ||
begin | ||
rw [linear_equiv.finrank_eq $ ideal.quotient_equiv_direct_sum F b hI, | ||
finite_dimensional.finrank_direct_sum] | ||
-- slow, and dot notation doesn't work | ||
end |
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 lemma might look unnecessary but I just tested and it can't be inlined in finrank_quotient_span_eq_nat_degree_norm
in #18000.
Thanks! bors merge |
…otient_eq_sum (#19084) Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
@Multramate, before you make many more mathlib3 PRs, please forward-port this and your other four changes (two PRs) on https://leanprover-community.github.io/mathlib-port-status/out-of-sync |
instance (F : Type u) [comm_ring F] [algebra F R] (b : basis ι R S) {I : ideal S} (hI : I ≠ ⊥) (i) : | ||
module F (R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R)) := | ||
by apply_instance -- quotient.module' _ | ||
|
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.
What was the purpose of adding this instance if apply_instance
can already find 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.
See #19084 (comment)
It's weird we need to add a shortcut instance that is already found by typeclass inference.
…4821) [`linear_algebra.free_module.ideal_quotient`@`6623e6af705e97002a9054c1c05a980180276fc1`..`d87199d51218d36a0a42c66c82d147b5a7ff87b3`](https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/free_module/ideal_quotient?range=6623e6af705e97002a9054c1c05a980180276fc1..d87199d51218d36a0a42c66c82d147b5a7ff87b3)
…4820) [`linear_algebra.free_module.pid`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`d87199d51218d36a0a42c66c82d147b5a7ff87b3`](https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/free_module/pid?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..d87199d51218d36a0a42c66c82d147b5a7ff87b3) Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
…eanprover-community#4821) [`linear_algebra.free_module.ideal_quotient`@`6623e6af705e97002a9054c1c05a980180276fc1`..`d87199d51218d36a0a42c66c82d147b5a7ff87b3`](https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/free_module/ideal_quotient?range=6623e6af705e97002a9054c1c05a980180276fc1..d87199d51218d36a0a42c66c82d147b5a7ff87b3)
…eanprover-community#4820) [`linear_algebra.free_module.pid`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`d87199d51218d36a0a42c66c82d147b5a7ff87b3`](https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/free_module/pid?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..d87199d51218d36a0a42c66c82d147b5a7ff87b3) Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Junyan Xu junyanxumath@gmail.com