quadratic_form): bilinear, quadratic forms on finsupp
#6606

Open

feat(linear_algebra/bilinear_form, linear_algebra/quadratic_form): bilinear, quadratic forms on finsupp #6606

hrmacbeth wants to merge 23 commits into master from finsupp_bilin

feat(linear_algebra/basic): add missing lemma finsupp.smul_sum'

c66bf06c

Update src/linear_algebra/basic.lean

29ebd124

Add Eric's `finsupp.sum_smul_index_add_monoid_hom`

d2a43c03

initial commit

40b9c02b

hrmacbeth added awaiting-review

github-actions added blocked-by-other-PR

eric-wieser commented on 2021-03-09

wip

d98d4799

fix

ee097a97

hrmacbeth changed the title ~~feat(linear_algebra/bilinear_form): bilinear form on finsupp~~ feat(linear_algebra/bilinear_form, linear_algebra/quadratic_form): bilinear, quadratic forms on finsupp 4 years ago

github-actions removed blocked-by-other-PR

github-actions added merge-conflict

Merge remote-tracking branch 'origin/master' into finsupp_bilin

68fb4b90

github-actions removed merge-conflict

fix

f7741d54

fix

8af77725

material on `flip` for bilinear forms

5ac3d6f5

rest of the term proofs

86639f40

fill smul sorry

f13be0f0

lint

b95c65cf

eric-wieser commented on 2021-03-14

Update src/linear_algebra/bilinear_form.lean

e07b12a8

Update src/linear_algebra/bilinear_form.lean

86915e8e

complete rename `bilin_form_of`

e637fbd0

remove hypothesis on map_sum_*/correct namespacing

5c34f6cb

eric-wieser commented on 2021-03-17

bryangingechen removed awaiting-review

bryangingechen added awaiting-author

Apply suggestions from code review

369d7d90

separate general-purpose changes from #6606

5d187e83

Merge branch 'to_lin_generalize' into finsupp_bilin

1f7cedfd

lemma linear_map.map_sum₂

0f1110fd

Merge branch 'to_lin_generalize' into finsupp_bilin

5a0daab1

github-actions added blocked-by-other-PR

github-actions added merge-conflict

github-actions removed blocked-by-other-PR

Merge remote-tracking branch 'origin/master' into finsupp_bilin

9a614116

github-actions removed merge-conflict

eric-wieser removed awaiting-author

eric-wieser added awaiting-review

Vierkantor requested a review from

Vierkantor 4 years ago

Vierkantor approved these changes on 2021-04-14

Vierkantor removed awaiting-review

Vierkantor added delegated

github-actions added merge-conflict

kim-em added too-late

Reviewers

Vierkantor

eric-wieser

tb65536

gebner

Assignees

No one assigned

Labels

delegated merge-conflict too-late

Milestone

No milestone

mathlib3 feat(linear_algebra/bilinear_form, linear_algebra/quadratic_form): bilinear, quadratic forms on finsupp #6606 Open

feat(linear_algebra/bilinear_form, linear_algebra/quadratic_form): bilinear, quadratic forms on finsupp #6606

mathlib3
feat(linear_algebra/bilinear_form, linear_algebra/quadratic_form): bilinear, quadratic forms on finsupp
#6606

Open