mathlib3
feat(algebra/*): morphisms from closures are equal if they agree on generators
#18836

Open

feat(algebra/*): morphisms from closures are equal if they agree on generators #18836

eric-wieser wants to merge 2 commits into master from eric-wieser/span-ext

feat(algebra/*): morphisms from closures are equal if they agree on g…

4ed70f0a

eric-wieser added awaiting-review

eric-wieser added awaiting-CI

eric-wieser added t-algebra

github-actions added modifies-synchronized-file

deduplicate, fix names

7012ca7c

eric-wieser commented on 2023-04-19

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-review awaiting-CI t-algebra modifies-synchronized-file too-late

Milestone

No milestone