This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
[Merged by Bors] - feat(algebra/direct_sum/decomposition): add an induction principle for direct_sum.decomposition class
#15654
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jjaassoonn
added
the
awaiting-review
2 tasks
hrmacbeth
changed the title
direct_sum.decomposition classdirect_sum.decomposition class
leanprover-community-bot-assistant
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jul 29, 2022
…r `direct_sum.decomposition` class (#15654) If `direct_sum.decomposition M` and `p : M → Prop`, then to prove `p m` for an arbitrary `m`, it suffices to prove `p 0` and `p x` for homogeneous x and `p` being preserved by add.
eric-wieser
reviewed
Jul 29, 2022
Comment on lines
+79
to
+80
| let ℳ' : ι → add_submonoid M := | ||
| λ i, (⟨ℳ i, λ _ _, add_mem_class.add_mem, zero_mem_class.zero_mem _⟩ : add_submonoid M), |
There was a problem hiding this comment.
This is another argument for addressing #15053 sooner rather than later; but no reason to cancel merging this PR.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
direct_sum.decomposition classdirect_sum.decomposition class
bottine
pushed a commit
to bottine/mathlib
that referenced
this pull request
Jul 30, 2022
…r `direct_sum.decomposition` class (leanprover-community#15654) If `direct_sum.decomposition M` and `p : M → Prop`, then to prove `p m` for an arbitrary `m`, it suffices to prove `p 0` and `p x` for homogeneous x and `p` being preserved by add.
robertylewis
pushed a commit
that referenced
this pull request
Aug 2, 2022
…r `direct_sum.decomposition` class (#15654) If `direct_sum.decomposition M` and `p : M → Prop`, then to prove `p m` for an arbitrary `m`, it suffices to prove `p 0` and `p x` for homogeneous x and `p` being preserved by add.
khwilson
pushed a commit
that referenced
this pull request
Aug 2, 2022
…r `direct_sum.decomposition` class (#15654) If `direct_sum.decomposition M` and `p : M → Prop`, then to prove `p m` for an arbitrary `m`, it suffices to prove `p 0` and `p x` for homogeneous x and `p` being preserved by add.
bors bot
pushed a commit
that referenced
this pull request
Jan 27, 2023
By imitating the current `graded_algebra`, this pr builds `graded_module` over some `graded algebra` Co-authored-by: Eric Wieser @eric-wieser - [x] depends on: #14626 - [x] depends on: #15654 Co-authored-by: Eric Wieser <[email protected]>
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
If
direct_sum.decomposition Mandp : M → Prop, then to provep mfor an arbitrarym, it suffices to provep 0andp xfor homogeneous x andpbeing preserved by add.