infinite_sum): Extract `none` from a sum over `option` types
#19150

Open

feat(topology/algebra/infinite_sum): Extract `none` from a sum over `option` types #19150

dtumad wants to merge 2 commits into master from tsum_option_lemmas

feat(topology/algebra/infinite_sum): Lemmas for sums over

0660a48d

dtumad added awaiting-review

github-actions added modifies-synchronized-file

dtumad commented on 2023-06-04

eric-wieser commented on 2023-06-04

eric-wieser changed the title ~~feat(topology/algebra/infinite_sum): Extract `none` from a some over `option` types~~ feat(topology/algebra/infinite_sum): Extract `none` from a sum over `option` types 2 years ago

eric-wieser removed awaiting-review

eric-wieser added awaiting-author

lemmas in terms of has_sum

c0afc9a0

dtumad removed awaiting-author

dtumad added awaiting-review

urkud commented on 2023-06-21

urkud removed awaiting-review

urkud added awaiting-author

kim-em added too-late

Reviewers

urkud

eric-wieser

Assignees

No one assigned

Labels

awaiting-author modifies-synchronized-file too-late

Milestone

No milestone

mathlib3 feat(topology/algebra/infinite_sum): Extract `none` from a sum over `option` types #19150 Open

feat(topology/algebra/infinite_sum): Extract `none` from a sum over `option` types #19150

mathlib3
feat(topology/algebra/infinite_sum): Extract `none` from a sum over `option` types
#19150

Open