basic): golf using injective APIs
#12676

Open

chore(topology/algebra/module/basic): golf using injective APIs #12676

eric-wieser wants to merge 4 commits into master from eric-wieser/continuous_linear_map-injective

chore(topology/algebra/module/basic): golf using injective APIs

7e39766e

eric-wieser added awaiting-review

argument order fix

fb807dbb

the cache is garbage, please rebuild it

de778db5

leanprover-community-bot-assistant added blocked-by-other-PR

leanprover-community-bot-assistant removed blocked-by-other-PR

leanprover-community-bot-assistant added merge-conflict

Merge branch 'master' into eric-wieser/continuous_linear_map-injective

62165e91

eric-wieser removed merge-conflict

eric-wieser added awaiting-CI

eric-wieser added help-wanted

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

help-wanted awaiting-review awaiting-CI too-late

Milestone

No milestone