Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

feat(topology/algebra/infinite_sum) : define infinite products - #19219

Open
AntoineChambert-Loir wants to merge 3 commits into
masterfrom
has_tprod
Open

feat(topology/algebra/infinite_sum) : define infinite products#19219
AntoineChambert-Loir wants to merge 3 commits into
masterfrom
has_tprod

Conversation

@AntoineChambert-Loir

Copy link
Copy Markdown
Collaborator

This is a refactor of infinite sums, more or less everything is now available in a comm_monoid via multipliable, has_tprod, tprod, and in the case of add_comm_monoid as smmable, has_sum, tsum.


Open in Gitpod

@AntoineChambert-Loir AntoineChambert-Loir added the awaiting-review The author would like community review of the PR label Jun 29, 2023
@github-actions github-actions Bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jun 29, 2023
@eric-wieser

Copy link
Copy Markdown
Member

As discussed on Zulip, we have a competing PR for this at #18405.

@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

awaiting-review The author would like community review of the PR modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. too-late This PR was ready too late for inclusion in mathlib3

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants