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.

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

Commits on Oct 5, 2023

  1. WIP on Quadratic Maps

    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 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 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 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 committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    e069e48 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    5e4ad04 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    c3d358e View commit details
    Browse the repository at this point in the history
  4. 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 committed Oct 8, 2023
    Configuration menu
    Copy the full SHA
    81cb2b3 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    8d4ca5d View commit details
    Browse the repository at this point in the history
  3. Remove some noise

    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 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 committed Oct 9, 2023
    Configuration menu
    Copy the full SHA
    60be27f View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    e59f746 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    e404bdc View commit details
    Browse the repository at this point in the history
  4. WiP

    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. Configuration menu
    Copy the full SHA
    51d2ef1 View commit details
    Browse the repository at this point in the history
  2. WIP

    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 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 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 committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    d9e5e81 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    b592bf3 View commit details
    Browse the repository at this point in the history
  7. Progress

    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 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 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 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 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 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 committed Oct 30, 2023
    Configuration menu
    Copy the full SHA
    bd36143 View commit details
    Browse the repository at this point in the history
  2. 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. 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. Configuration menu
    Copy the full SHA
    3f12e8e View commit details
    Browse the repository at this point in the history
  2. 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. 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. 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. Configuration menu
    Copy the full SHA
    d986a30 View commit details
    Browse the repository at this point in the history
  2. Fix

    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 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 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 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. Configuration menu
    Copy the full SHA
    b9faabb View commit details
    Browse the repository at this point in the history
  2. 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. 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 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 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 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 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 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    76d42ba View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    1c93859 View commit details
    Browse the repository at this point in the history
  7. BilinMap and BilinForm

    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. 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 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 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 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 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 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 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    9e417dd View commit details
    Browse the repository at this point in the history
  15. 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 committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    63145ac View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    446ff4d View commit details
    Browse the repository at this point in the history
  3. Update yaml

    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 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 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 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 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 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 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 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 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 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 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 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 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 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 committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    0144093 View commit details
    Browse the repository at this point in the history
  13. 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. 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 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 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    aad903b View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    55a472e View commit details
    Browse the repository at this point in the history
  3. 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 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 committed Apr 26, 2024
    Configuration menu
    Copy the full SHA
    5f7efa3 View commit details
    Browse the repository at this point in the history
  3. 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 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    9805ded View commit details
    Browse the repository at this point in the history
  2. 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 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    475f67b View commit details
    Browse the repository at this point in the history
  4. 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 committed Apr 28, 2024
    Configuration menu
    Copy the full SHA
    63b3270 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    0e37c06 View commit details
    Browse the repository at this point in the history
  7. Remove variable

    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. 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. Configuration menu
    Copy the full SHA
    ddae0dd View commit details
    Browse the repository at this point in the history
  2. Fix

    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. 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. 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. Configuration menu
    Copy the full SHA
    7f5e47e View commit details
    Browse the repository at this point in the history
  2. Fix

    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. Configuration menu
    Copy the full SHA
    35cd288 View commit details
    Browse the repository at this point in the history
  2. Fix

    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. 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. 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. 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. Configuration menu
    Copy the full SHA
    63cce90 View commit details
    Browse the repository at this point in the history
  2. Remove dup

    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. Configuration menu
    Copy the full SHA
    a4ba875 View commit details
    Browse the repository at this point in the history
  2. Fix

    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 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. 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. Configuration menu
    Copy the full SHA
    411786f View commit details
    Browse the repository at this point in the history
  2. 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. Configuration menu
    Copy the full SHA
    4aa7ee0 View commit details
    Browse the repository at this point in the history
  2. remove _root_

    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 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 committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    3c60a70 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    6027e18 View commit details
    Browse the repository at this point in the history
  6. Get it building

    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. Configuration menu
    Copy the full SHA
    d45b144 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    6a8e48f View commit details
    Browse the repository at this point in the history
  9. 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. Configuration menu
    Copy the full SHA
    255b66f View commit details
    Browse the repository at this point in the history
  2. reduce diff

    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 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 committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    6830b5f View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    6e3c99b View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    102aa6b View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    d6e19c6 View commit details
    Browse the repository at this point in the history
  6. 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 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. 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 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 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. Configuration menu
    Copy the full SHA
    2afbdd0 View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    6835243 View commit details
    Browse the repository at this point in the history
  13. Configuration menu
    Copy the full SHA
    4b97ea0 View commit details
    Browse the repository at this point in the history
  14. Configuration menu
    Copy the full SHA
    7857382 View commit details
    Browse the repository at this point in the history
  15. Configuration menu
    Copy the full SHA
    3c714d3 View commit details
    Browse the repository at this point in the history
  16. Configuration menu
    Copy the full SHA
    3774529 View commit details
    Browse the repository at this point in the history
  17. 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 committed Jul 13, 2024
    Configuration menu
    Copy the full SHA
    9b5284b View commit details
    Browse the repository at this point in the history
  19. Configuration menu
    Copy the full SHA
    2532a7b View commit details
    Browse the repository at this point in the history