[Merged by Bors] - feat(ring_theory/hahn_series): order of a nonzero Hahn series, reindexing summable families #7444
Conversation
awainverse
added
the
awaiting-review
jcommelin
added
awaiting-author
awainverse
added
awaiting-review
| @@ -700,4 +700,16 @@ lemma finsum_mul {R : Type*} [semiring R] (f : α → R) (r : R) | |||
| (∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r := | |||
| (add_monoid_hom.mul_right r).map_finsum h | |||
|
|
|||
| @[to_additive] | |||
| lemma finprod_emb_domain (f : α ↪ β) [decidable_pred (∈ set.range f)] (g : α → M) : | |||
| ∏ᶠ (b : β), (if h : b ∈ set.range f then g (classical.some h) else 1) = ∏ᶠ (a : α), g a := | |||
There was a problem hiding this comment.
The left hand side looks rather complicated and specialized. Do you think this could be replaced with the indicator function on the range of f? Also, I can imagine that someone will want to rw with this lemma, but only has an ordinary function that is function.injective. Would you mind also providing that version?
There was a problem hiding this comment.
I can definitely do an injective version, but I'm having trouble determining what other form this could take. It's not equivalent to just an indicator function, because the thing being summed over depends on h : b ∈ set.range f. Perhaps a general classical.some lemma is the greatest generality?
There was a problem hiding this comment.
I've made a helper lemma that does most of the work, by allowing you to convert between a finprod_mem that depends on the actual mem statement and one that does not, but I've left the original statement put. I expect it will find more use than just this, because if we end up refactoring finsupp to use finsum, this is the critical idea behind summing finsupp.emb_domain.
jcommelin
added
awaiting-author
awainverse
added
awaiting-review
jcommelin
added
awaiting-author
awainverse
added
awaiting-review
|
Great! If it passes CI, please merge it. bors d+ |
|
✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
…xing summable families (#7444) Defines `hahn_series.order`, the order of a nonzero Hahn series Restates `add_val` in terms of `hahn_series.order` Defines `hahn_series.summable_family.emb_domain`, reindexing a summable family using an embedding
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Defines
hahn_series.order, the order of a nonzero Hahn seriesRestates
add_valin terms ofhahn_series.orderDefines
hahn_series.summable_family.emb_domain, reindexing a summable family using an embeddingThe two things being introduced in this PR are not directly related, but they are both fairly straightforward, and came up in defining the field structure.