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

Jump to bottom

[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

wants to merge 141 commits into from

Commits on Oct 5, 2023

  1. WIP on Quadratic Maps

    @mans0954
    mans0954 committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    22eff29 View commit details
    Browse the repository at this point in the history

  2. More

    @mans0954
    mans0954 committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    08e698a View commit details
    Browse the repository at this point in the history

  3. More

    @mans0954
    mans0954 committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    9c113e8 View commit details
    Browse the repository at this point in the history

  4. Weaken hypothesis

    @mans0954
    mans0954 committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    f6a70e1 View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2023

  1. Don't need extra import

    @mans0954
    mans0954 committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    e069e48 View commit details
    Browse the repository at this point in the history

  2. Don't need SMulCommClass condition on R₂

    @mans0954
    mans0954 committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    5e4ad04 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into mans0954/Bilinear-SMulCommClass

    @mans0954
    mans0954 committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    c3d358e View commit details
    Browse the repository at this point in the history

  4. Merge branch 'mans0954/Bilinear-SMulCommClass' into mans0954/quadrati… 

    …c-maps
    @mans0954
    mans0954 committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    635619b View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2023

  1. Add more SMulCommClass

    @mans0954
    mans0954 committed Oct 8, 2023
    Configuration menu
    Copy the full SHA
    81cb2b3 View commit details
    Browse the repository at this point in the history

  2. Remove changes to BilinearMap

    @mans0954
    mans0954 committed Oct 8, 2023
    Configuration menu
    Copy the full SHA
    8d4ca5d View commit details
    Browse the repository at this point in the history

  3. Remove some noise

    @mans0954
    mans0954 committed Oct 8, 2023
    Configuration menu
    Copy the full SHA
    ad25eb1 View commit details
    Browse the repository at this point in the history

  4. Lint

    @mans0954
    mans0954 committed Oct 8, 2023
    Configuration menu
    Copy the full SHA
    3effb8e View commit details
    Browse the repository at this point in the history

Commits on Oct 9, 2023

  1. Resync to master

    @mans0954
    mans0954 committed Oct 9, 2023
    Configuration menu
    Copy the full SHA
    60be27f View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Oct 9, 2023
    Configuration menu
    Copy the full SHA
    e59f746 View commit details
    Browse the repository at this point in the history

  3. Get us back to where we were

    @mans0954
    mans0954 committed Oct 9, 2023
    Configuration menu
    Copy the full SHA
    e404bdc View commit details
    Browse the repository at this point in the history

  4. WiP

    @mans0954
    mans0954 committed Oct 9, 2023
    Configuration menu
    Copy the full SHA
    2c611ce View commit details
    Browse the repository at this point in the history

Commits on Oct 26, 2023

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    51d2ef1 View commit details
    Browse the repository at this point in the history

  2. WIP

    @mans0954
    mans0954 committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    bc1b52e View commit details
    Browse the repository at this point in the history

  3. Missed this earlier

    @mans0954
    mans0954 committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    ab540ab View commit details
    Browse the repository at this point in the history

  4. Progress

    @mans0954
    mans0954 committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    ef3c9cb View commit details
    Browse the repository at this point in the history

  5. Lint

    @mans0954
    mans0954 committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    d9e5e81 View commit details
    Browse the repository at this point in the history

  6. QuadraticForm.polarBilin_injective

    @mans0954
    mans0954 committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    b592bf3 View commit details
    Browse the repository at this point in the history

  7. Progress

    @mans0954
    mans0954 committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    a7e111e View commit details
    Browse the repository at this point in the history

  8. Lint

    @mans0954
    mans0954 committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    0d8a49c View commit details
    Browse the repository at this point in the history

Commits on Oct 27, 2023

  1. WIP

    @mans0954
    mans0954 committed Oct 27, 2023
    Configuration menu
    Copy the full SHA
    313469d View commit details
    Browse the repository at this point in the history

  2. WiP

    @mans0954
    mans0954 committed Oct 27, 2023
    Configuration menu
    Copy the full SHA
    0809e18 View commit details
    Browse the repository at this point in the history

  3. WiP

    @mans0954
    mans0954 committed Oct 27, 2023
    Configuration menu
    Copy the full SHA
    d5da8b1 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2023

  1. PosDef

    @mans0954
    mans0954 committed Oct 29, 2023
    Configuration menu
    Copy the full SHA
    adf9969 View commit details
    Browse the repository at this point in the history

Commits on Oct 30, 2023

  1. Notes on matrices

    @mans0954
    mans0954 committed Oct 30, 2023
    Configuration menu
    Copy the full SHA
    bd36143 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Oct 30, 2023
    Configuration menu
    Copy the full SHA
    51e37b4 View commit details
    Browse the repository at this point in the history

Commits on Nov 19, 2023

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    6323478 View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2023

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Dec 4, 2023
    Configuration menu
    Copy the full SHA
    3f12e8e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Dec 4, 2023
    Configuration menu
    Copy the full SHA
    93c24f1 View commit details
    Browse the repository at this point in the history

Commits on Dec 23, 2023

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Dec 23, 2023
    Configuration menu
    Copy the full SHA
    653079d View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    dabc47b View commit details
    Browse the repository at this point in the history

Commits on Jan 23, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    d986a30 View commit details
    Browse the repository at this point in the history

  2. Fix

    @mans0954
    mans0954 committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    3839265 View commit details
    Browse the repository at this point in the history

  3. IsOrtho/CommSemiring

    @mans0954
    mans0954 committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    ef09743 View commit details
    Browse the repository at this point in the history

  4. AssociatedHom

    @mans0954
    mans0954 committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    b3ecfd6 View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2024

  1. Associated

    @mans0954
    mans0954 committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    66d29d1 View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    b9faabb View commit details
    Browse the repository at this point in the history

  2. Remove duplicate invOf_smul_eq_iff

    @mans0954
    mans0954 committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    e9b7360 View commit details
    Browse the repository at this point in the history

Commits on Mar 29, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Mar 29, 2024
    Configuration menu
    Copy the full SHA
    26f97ea View commit details
    Browse the repository at this point in the history

Commits on Apr 4, 2024

  1. Replace add_sub_cancel'

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    ace1123 View commit details
    Browse the repository at this point in the history

  2. Tidy

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    969a79e View commit details
    Browse the repository at this point in the history

  3. Make more use of BilinMap

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    172e9c6 View commit details
    Browse the repository at this point in the history

  4. Tidy

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    12059c0 View commit details
    Browse the repository at this point in the history

  5. Fix

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    76d42ba View commit details
    Browse the repository at this point in the history

  6. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    1c93859 View commit details
    Browse the repository at this point in the history

  7. BilinMap and BilinForm

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    a640495 View commit details
    Browse the repository at this point in the history

  8. Rename QuadraticForm to QuadraticMap

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    54ce9b4 View commit details
    Browse the repository at this point in the history

  9. Fix up the rest of Mathlib

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    37f4d06 View commit details
    Browse the repository at this point in the history

  10. Fix counter example

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    d0b7e63 View commit details
    Browse the repository at this point in the history

  11. Fix counter example

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    80626e0 View commit details
    Browse the repository at this point in the history

  12. Add docstring

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    2560494 View commit details
    Browse the repository at this point in the history

  13. No Doc

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    1faf61f View commit details
    Browse the repository at this point in the history

  14. remove unused arg

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    9e417dd View commit details
    Browse the repository at this point in the history

  15. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    571492d View commit details
    Browse the repository at this point in the history

Commits on Apr 5, 2024

  1. Remove check

    @mans0954
    mans0954 committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    63145ac View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    446ff4d View commit details
    Browse the repository at this point in the history

  3. Update yaml

    @mans0954
    mans0954 committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    b4d324d View commit details
    Browse the repository at this point in the history

  4. Update docstrings

    @mans0954
    mans0954 committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    e6c4b2a View commit details
    Browse the repository at this point in the history

  5. Tidy

    @mans0954
    mans0954 committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    64b088e View commit details
    Browse the repository at this point in the history

Commits on Apr 9, 2024

  1. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    05c60f2 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    d42d592 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    2c356d3 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    5b613f5 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    5228893 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    0526c72 View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    ff74bfc View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    bdc3564 View commit details
    Browse the repository at this point in the history

  9. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    af7f32b View commit details
    Browse the repository at this point in the history

  10. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Mitchell Lee <[email protected]>
    @mans0954 @trivial1711
    mans0954 and trivial1711 authored Apr 9, 2024
    Configuration menu
    Copy the full SHA
    e525e23 View commit details
    Browse the repository at this point in the history

  11. Fix

    @mans0954
    mans0954 committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    29b71bb View commit details
    Browse the repository at this point in the history

  12. map_add_self

    @mans0954
    mans0954 committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    0144093 View commit details
    Browse the repository at this point in the history

  13. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    17bc77c View commit details
    Browse the repository at this point in the history

Commits on Apr 14, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Apr 14, 2024
    Configuration menu
    Copy the full SHA
    f48dcc2 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/LinearAlgebra/BilinearMap.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser authored Apr 14, 2024
    Configuration menu
    Copy the full SHA
    e9b0cc1 View commit details
    Browse the repository at this point in the history

Commits on Apr 19, 2024

  1. PosDef for Quadratic Maps

    @mans0954
    mans0954 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    aad903b View commit details
    Browse the repository at this point in the history

  2. Convert linMulLin to Quadratic Maps

    @mans0954
    mans0954 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    55a472e View commit details
    Browse the repository at this point in the history

  3. Make linMulLinSelfPosDef work for maps

    @mans0954
    mans0954 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    3f1e782 View commit details
    Browse the repository at this point in the history

Commits on Apr 26, 2024

  1. Ready for non-assoc

    @mans0954
    mans0954 committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    6df6e28 View commit details
    Browse the repository at this point in the history

  2. Lint

    @mans0954
    mans0954 committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    5f7efa3 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    d2799ae View commit details
    Browse the repository at this point in the history

Commits on Apr 28, 2024

  1. fix after merge

    @mans0954
    mans0954 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    9805ded View commit details
    Browse the repository at this point in the history

  2. Add toNonUnitalNonAssocCommSemiring instance

    @mans0954
    mans0954 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    2beed79 View commit details
    Browse the repository at this point in the history

  3. Revert "Add toNonUnitalNonAssocCommSemiring instance" 

    This reverts commit 2beed79.
    @mans0954
    mans0954 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    475f67b View commit details
    Browse the repository at this point in the history

  4. Add CommSemiring.toNonUnitalNonAssocCommSemiring to the wrong place

    @mans0954
    mans0954 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    92406c6 View commit details
    Browse the repository at this point in the history

  5. Rename N' to M'

    @mans0954
    mans0954 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    63b3270 View commit details
    Browse the repository at this point in the history

  6. Split compQuadraticMap into a composition

    @mans0954
    mans0954 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    0e37c06 View commit details
    Browse the repository at this point in the history

  7. Remove variable

    @mans0954
    mans0954 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    cff4d4e View commit details
    Browse the repository at this point in the history

Commits on May 2, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed May 2, 2024
    Configuration menu
    Copy the full SHA
    352cdd8 View commit details
    Browse the repository at this point in the history

Commits on May 3, 2024

  1. Use A in NonUnitalNonAssocCommSemiring

    @mans0954
    mans0954 committed May 3, 2024
    Configuration menu
    Copy the full SHA
    ddae0dd View commit details
    Browse the repository at this point in the history

  2. Fix

    @mans0954
    mans0954 committed May 3, 2024
    Configuration menu
    Copy the full SHA
    f45042a View commit details
    Browse the repository at this point in the history

  3. Use A in linMulLinSelfPosDef as well

    @mans0954
    mans0954 committed May 3, 2024
    Configuration menu
    Copy the full SHA
    6234f0c View commit details
    Browse the repository at this point in the history

Commits on May 4, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed May 4, 2024
    Configuration menu
    Copy the full SHA
    2181220 View commit details
    Browse the repository at this point in the history

Commits on May 7, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed May 7, 2024
    Configuration menu
    Copy the full SHA
    7f5e47e View commit details
    Browse the repository at this point in the history

  2. Fix

    @mans0954
    mans0954 committed May 7, 2024
    Configuration menu
    Copy the full SHA
    ae01d41 View commit details
    Browse the repository at this point in the history

Commits on May 19, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed May 19, 2024
    Configuration menu
    Copy the full SHA
    35cd288 View commit details
    Browse the repository at this point in the history

  2. Fix

    @mans0954
    mans0954 committed May 19, 2024
    Configuration menu
    Copy the full SHA
    b230323 View commit details
    Browse the repository at this point in the history

Commits on May 22, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed May 22, 2024
    Configuration menu
    Copy the full SHA
    fba9c62 View commit details
    Browse the repository at this point in the history

Commits on May 25, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed May 25, 2024
    Configuration menu
    Copy the full SHA
    16c96a6 View commit details
    Browse the repository at this point in the history

Commits on Jun 1, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    b82e978 View commit details
    Browse the repository at this point in the history

Commits on Jun 6, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Jun 6, 2024
    Configuration menu
    Copy the full SHA
    63cce90 View commit details
    Browse the repository at this point in the history

  2. Remove dup

    @mans0954
    mans0954 committed Jun 6, 2024
    Configuration menu
    Copy the full SHA
    6bb68b8 View commit details
    Browse the repository at this point in the history

Commits on Jun 7, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Jun 7, 2024
    Configuration menu
    Copy the full SHA
    a4ba875 View commit details
    Browse the repository at this point in the history

  2. Fix

    @mans0954
    mans0954 committed Jun 7, 2024
    Configuration menu
    Copy the full SHA
    18f1e3e View commit details
    Browse the repository at this point in the history

  3. Fix

    @mans0954
    mans0954 committed Jun 7, 2024
    Configuration menu
    Copy the full SHA
    6955ed5 View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Jul 2, 2024
    Configuration menu
    Copy the full SHA
    e10cf6d View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @eric-wieser
    eric-wieser authored Jul 10, 2024
    Configuration menu
    Copy the full SHA
    411786f View commit details
    Browse the repository at this point in the history

  2. chore: protect QuadraticForm.map_zero

    @eric-wieser
    eric-wieser committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    69296c6 View commit details
    Browse the repository at this point in the history

Commits on Jul 11, 2024

  1. Merge branch 'eric-wieser/quadraticform-map_zero' into mans0954/quadr… 

    …atic-maps
    @eric-wieser
    eric-wieser committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    4aa7ee0 View commit details
    Browse the repository at this point in the history

  2. remove _root_

    @eric-wieser
    eric-wieser committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    5605771 View commit details
    Browse the repository at this point in the history

  3. prune typeclasses

    @eric-wieser
    eric-wieser committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    3e88792 View commit details
    Browse the repository at this point in the history

  4. unused arguments

    @eric-wieser
    eric-wieser committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    3c60a70 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/master' into mans0954/quadratic-… 

    …maps
    @eric-wieser
    eric-wieser committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    6027e18 View commit details
    Browse the repository at this point in the history

  6. Get it building

    @mans0954
    mans0954 committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    9b9ccc1 View commit details
    Browse the repository at this point in the history

  7. Rename compQuadraticMap to compQuadraticMap'

    @mans0954
    mans0954 committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    d45b144 View commit details
    Browse the repository at this point in the history

  8. rename compQuadraticMapAux to compQuadraticMap

    @mans0954
    mans0954 committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    6a8e48f View commit details
    Browse the repository at this point in the history

  9. Restrict linMulLin to unital assoc case for now

    @mans0954
    mans0954 committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    d025c1c View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2024

  1. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    255b66f View commit details
    Browse the repository at this point in the history

  2. reduce diff

    @eric-wieser
    eric-wieser committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    18f9235 View commit details
    Browse the repository at this point in the history

Commits on Jul 13, 2024

  1. tidy variables

    @eric-wieser
    eric-wieser committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    8aa26b3 View commit details
    Browse the repository at this point in the history

  2. commutativity not needed

    @eric-wieser
    eric-wieser committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    6830b5f View commit details
    Browse the repository at this point in the history

  3. drop commutativity one more time

    @eric-wieser
    eric-wieser committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    6e3c99b View commit details
    Browse the repository at this point in the history

  4. heartbeat limit not needed

    @eric-wieser
    eric-wieser committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    102aa6b View commit details
    Browse the repository at this point in the history

  5. Optimistically remove set_option synthInstance.maxHeartbeats 7000 in

    @eric-wieser
    eric-wieser committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    d6e19c6 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/master' into mans0954/quadratic-… 

    …maps
    @eric-wieser
    eric-wieser committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    2410793 View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/LinearAlgebra/BilinearMap.lean 

    Co-authored-by: Michael Stoll <[email protected]>
    @mans0954 @MichaelStollBayreuth
    mans0954 and MichaelStollBayreuth authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    3113a24 View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Michael Stoll <[email protected]>
    @mans0954 @MichaelStollBayreuth
    mans0954 and MichaelStollBayreuth authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    0d8e1bc View commit details
    Browse the repository at this point in the history

  9. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    4df84ce View commit details
    Browse the repository at this point in the history

  10. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    ffc3c1d View commit details
    Browse the repository at this point in the history

  11. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Michael Stoll <[email protected]>
    @mans0954 @MichaelStollBayreuth
    mans0954 and MichaelStollBayreuth authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    2afbdd0 View commit details
    Browse the repository at this point in the history

  12. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Michael Stoll <[email protected]>
    @mans0954 @MichaelStollBayreuth
    mans0954 and MichaelStollBayreuth authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    6835243 View commit details
    Browse the repository at this point in the history

  13. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Michael Stoll <[email protected]>
    @mans0954 @MichaelStollBayreuth
    mans0954 and MichaelStollBayreuth authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    4b97ea0 View commit details
    Browse the repository at this point in the history

  14. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Michael Stoll <[email protected]>
    @mans0954 @MichaelStollBayreuth
    mans0954 and MichaelStollBayreuth authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    7857382 View commit details
    Browse the repository at this point in the history

  15. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Michael Stoll <[email protected]>
    @mans0954 @MichaelStollBayreuth
    mans0954 and MichaelStollBayreuth authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    3c714d3 View commit details
    Browse the repository at this point in the history

  16. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Michael Stoll <[email protected]>
    @mans0954 @MichaelStollBayreuth
    mans0954 and MichaelStollBayreuth authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    3774529 View commit details
    Browse the repository at this point in the history

  17. Update Mathlib/LinearAlgebra/QuadraticForm/Basic.lean 

    Co-authored-by: Michael Stoll <[email protected]>
    @mans0954 @MichaelStollBayreuth
    mans0954 and MichaelStollBayreuth authored Jul 13, 2024
    Configuration menu
    Copy the full SHA
    7e879da View commit details
    Browse the repository at this point in the history

  18. Explain what N is

    @mans0954
    mans0954 committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    9b5284b View commit details
    Browse the repository at this point in the history

  19. Merge branch 'master' into mans0954/quadratic-maps

    @mans0954
    mans0954 committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    2532a7b View commit details
    Browse the repository at this point in the history