multilinear): partially generalize to `semi_normed_group`
#13566

Open

feat(analysis/normed_space/multilinear): partially generalize to `semi_normed_group` #13566

eric-wieser wants to merge 9 commits into master from eric-wieser/semi_normed_ring

feat(analysis/normed_space/multilinear): generalize a few results to …

2e800920

generalize the codomain

75d9a543

eric-wieser added awaiting-author

eric-wieser added awaiting-CI

fix

4b48dbfb

line lengths

f56c7ca5

fix

182623c5

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 remote-tracking branch 'origin/master' into eric-wieser/semi_no…

d5eaadb9

leanprover-community-bot-assistant removed merge-conflict

fix bad merge

7348fe84

this didn't help

b88bb787

Merge remote-tracking branch 'origin/master' into eric-wieser/semi_no…

b629a3dc

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-author awaiting-CI too-late

Milestone

No milestone