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
feat(ring_theory/graded_ring): basics #10002
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…b.com/leanprover-community/mathlib into feat(homogenous-ideal-of-graded-ring)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…b.com/leanprover-community/mathlib into feat(homogenous-ideal-of-graded-ring)
I am going to split this pr into smaller ones. |
lemma graded_ring.trivial_inter (i : ι) : | ||
disjoint (A i) (Sup {a | ∃ j ≠ i, A j = a}) := |
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 should fall out in a line or two from #10108. If it doesn't, there's a lemma missing from the API of complete_lattice.independent
.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Now every sub-pr is <150 lines modulo dependencies. |
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
This pr is now being subsumed by other sub prs. So I will close this one |
This pr is about typeclasse of graded ring
Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/graded.20rings
direct_sum.of
#10003Definitions of
graded_ring
graded_algebra
#10115Definition of
proj
and its propertiesproj
#10121Definition of
homogeneous_element
homogeneous_element
#10118submodule_is_internal.independent
to add_subgroup #10108If I copy and pasted correctly, these sub-prs should be everything this pr has.