Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise QuadraticForm to QuadraticMap #7569

Closed
wants to merge 141 commits into from
Closed

[Merged by Bors] - refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise QuadraticForm to QuadraticMap #7569

Changes from 12 commits
Commits
Show all changes
141 commits
Select commit Hold shift + click to select a range
22eff29
WIP on Quadratic Maps
mans0954 Oct 5, 2023
08e698a
More
mans0954 Oct 5, 2023
9c113e8
More
mans0954 Oct 5, 2023
f6a70e1
Weaken hypothesis
mans0954 Oct 5, 2023
e069e48
Don't need extra import
mans0954 Oct 6, 2023
5e4ad04
Don't need SMulCommClass condition on R₂
mans0954 Oct 6, 2023
c3d358e
Merge branch 'master' into mans0954/Bilinear-SMulCommClass
mans0954 Oct 6, 2023
635619b
Merge branch 'mans0954/Bilinear-SMulCommClass' into mans0954/quadrati…
mans0954 Oct 6, 2023
81cb2b3
Add more SMulCommClass
mans0954 Oct 8, 2023
8d4ca5d
Remove changes to BilinearMap
mans0954 Oct 8, 2023
ad25eb1
Remove some noise
mans0954 Oct 8, 2023
3effb8e
Lint
mans0954 Oct 8, 2023
60be27f
Resync to master
mans0954 Oct 9, 2023
e59f746
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Oct 9, 2023
e404bdc
Get us back to where we were
mans0954 Oct 9, 2023
2c611ce
WiP
mans0954 Oct 9, 2023
51d2ef1
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Oct 26, 2023
bc1b52e
WIP
mans0954 Oct 26, 2023
ab540ab
Missed this earlier
mans0954 Oct 26, 2023
ef3c9cb
Progress
mans0954 Oct 26, 2023
d9e5e81
Lint
mans0954 Oct 26, 2023
b592bf3
QuadraticForm.polarBilin_injective
mans0954 Oct 26, 2023
a7e111e
Progress
mans0954 Oct 26, 2023
0d8a49c
Lint
mans0954 Oct 26, 2023
313469d
WIP
mans0954 Oct 27, 2023
0809e18
WiP
mans0954 Oct 27, 2023
d5da8b1
WiP
mans0954 Oct 27, 2023
adf9969
PosDef
mans0954 Oct 29, 2023
bd36143
Notes on matrices
mans0954 Oct 30, 2023
51e37b4
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Oct 30, 2023
6323478
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Nov 19, 2023
3f12e8e
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Dec 4, 2023
93c24f1
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Dec 4, 2023
653079d
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Dec 23, 2023
dabc47b
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Jan 5, 2024
d986a30
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Jan 23, 2024
3839265
Fix
mans0954 Jan 23, 2024
ef09743
IsOrtho/CommSemiring
mans0954 Jan 23, 2024
b3ecfd6
AssociatedHom
mans0954 Jan 23, 2024
66d29d1
Associated
mans0954 Jan 24, 2024
b9faabb
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Jan 27, 2024
e9b7360
Remove duplicate invOf_smul_eq_iff
mans0954 Jan 27, 2024
26f97ea
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Mar 29, 2024
ace1123
Replace add_sub_cancel'
mans0954 Apr 4, 2024
969a79e
Tidy
mans0954 Apr 4, 2024
172e9c6
Make more use of BilinMap
mans0954 Apr 4, 2024
12059c0
Tidy
mans0954 Apr 4, 2024
76d42ba
Fix
mans0954 Apr 4, 2024
1c93859
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Apr 4, 2024
a640495
BilinMap and BilinForm
mans0954 Apr 4, 2024
54ce9b4
Rename QuadraticForm to QuadraticMap
mans0954 Apr 4, 2024
37f4d06
Fix up the rest of Mathlib
mans0954 Apr 4, 2024
d0b7e63
Fix counter example
mans0954 Apr 4, 2024
80626e0
Fix counter example
mans0954 Apr 4, 2024
2560494
Add docstring
mans0954 Apr 4, 2024
1faf61f
No Doc
mans0954 Apr 4, 2024
9e417dd
remove unused arg
mans0954 Apr 4, 2024
571492d
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Apr 4, 2024
63145ac
Remove check
mans0954 Apr 5, 2024
446ff4d
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Apr 5, 2024
b4d324d
Update yaml
mans0954 Apr 5, 2024
e6c4b2a
Update docstrings
mans0954 Apr 5, 2024
64b088e
Tidy
mans0954 Apr 5, 2024
05c60f2
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
d42d592
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
2c356d3
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
5b613f5
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
5228893
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
0526c72
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
ff74bfc
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
bdc3564
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
af7f32b
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
e525e23
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Apr 9, 2024
29b71bb
Fix
mans0954 Apr 9, 2024
0144093
map_add_self
mans0954 Apr 9, 2024
17bc77c
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Apr 9, 2024
f48dcc2
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Apr 14, 2024
e9b0cc1
Update Mathlib/LinearAlgebra/BilinearMap.lean
mans0954 Apr 14, 2024
aad903b
PosDef for Quadratic Maps
mans0954 Apr 19, 2024
55a472e
Convert linMulLin to Quadratic Maps
mans0954 Apr 19, 2024
3f1e782
Make linMulLinSelfPosDef work for maps
mans0954 Apr 19, 2024
6df6e28
Ready for non-assoc
mans0954 Apr 20, 2024
5f7efa3
Lint
mans0954 Apr 26, 2024
d2799ae
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Apr 26, 2024
9805ded
fix after merge
mans0954 Apr 28, 2024
2beed79
Add toNonUnitalNonAssocCommSemiring instance
mans0954 Apr 28, 2024
475f67b
Revert "Add toNonUnitalNonAssocCommSemiring instance"
mans0954 Apr 28, 2024
92406c6
Add CommSemiring.toNonUnitalNonAssocCommSemiring to the wrong place
mans0954 Apr 28, 2024
63b3270
Rename N' to M'
mans0954 Apr 28, 2024
0e37c06
Split compQuadraticMap into a composition
mans0954 Apr 28, 2024
cff4d4e
Remove variable
mans0954 Apr 28, 2024
352cdd8
Merge branch 'master' into mans0954/quadratic-maps
mans0954 May 2, 2024
ddae0dd
Use A in NonUnitalNonAssocCommSemiring
mans0954 May 3, 2024
f45042a
Fix
mans0954 May 3, 2024
6234f0c
Use A in linMulLinSelfPosDef as well
mans0954 May 3, 2024
2181220
Merge branch 'master' into mans0954/quadratic-maps
mans0954 May 4, 2024
7f5e47e
Merge branch 'master' into mans0954/quadratic-maps
mans0954 May 7, 2024
ae01d41
Fix
mans0954 May 7, 2024
35cd288
Merge branch 'master' into mans0954/quadratic-maps
mans0954 May 19, 2024
b230323
Fix
mans0954 May 19, 2024
fba9c62
Merge branch 'master' into mans0954/quadratic-maps
mans0954 May 22, 2024
16c96a6
Merge branch 'master' into mans0954/quadratic-maps
mans0954 May 25, 2024
b82e978
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Jun 1, 2024
63cce90
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Jun 6, 2024
6bb68b8
Remove dup
mans0954 Jun 6, 2024
a4ba875
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Jun 7, 2024
18f1e3e
Fix
mans0954 Jun 7, 2024
6955ed5
Fix
mans0954 Jun 7, 2024
e10cf6d
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Jul 2, 2024
411786f
Merge branch 'master' into mans0954/quadratic-maps
eric-wieser Jul 10, 2024
69296c6
chore: protect `QuadraticForm.map_zero`
eric-wieser Jul 10, 2024
4aa7ee0
Merge branch 'eric-wieser/quadraticform-map_zero' into mans0954/quadr…
eric-wieser Jul 11, 2024
5605771
remove _root_
eric-wieser Jul 11, 2024
3e88792
prune typeclasses
eric-wieser Jul 11, 2024
3c60a70
unused arguments
eric-wieser Jul 11, 2024
6027e18
Merge remote-tracking branch 'origin/master' into mans0954/quadratic-…
eric-wieser Jul 11, 2024
9b9ccc1
Get it building
mans0954 Jul 11, 2024
d45b144
Rename compQuadraticMap to compQuadraticMap'
mans0954 Jul 11, 2024
6a8e48f
rename compQuadraticMapAux to compQuadraticMap
mans0954 Jul 11, 2024
d025c1c
Restrict linMulLin to unital assoc case for now
mans0954 Jul 11, 2024
255b66f
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Jul 12, 2024
18f9235
reduce diff
eric-wieser Jul 12, 2024
8aa26b3
tidy variables
eric-wieser Jul 13, 2024
6830b5f
commutativity not needed
eric-wieser Jul 13, 2024
6e3c99b
drop commutativity one more time
eric-wieser Jul 13, 2024
102aa6b
heartbeat limit not needed
eric-wieser Jul 13, 2024
d6e19c6
Optimistically remove `set_option synthInstance.maxHeartbeats 7000 in`
eric-wieser Jul 13, 2024
2410793
Merge remote-tracking branch 'origin/master' into mans0954/quadratic-…
eric-wieser Jul 13, 2024
3113a24
Update Mathlib/LinearAlgebra/BilinearMap.lean
mans0954 Jul 13, 2024
0d8e1bc
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
4df84ce
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
ffc3c1d
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
2afbdd0
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
6835243
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
4b97ea0
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
7857382
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
3c714d3
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
3774529
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
7e879da
Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
mans0954 Jul 13, 2024
9b5284b
Explain what N is
mans0954 Jul 13, 2024
2532a7b
Merge branch 'master' into mans0954/quadratic-maps
mans0954 Jul 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading