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): Replace BilinForm with a scalar valued bi LinearMap #10238

Closed
wants to merge 70 commits into from
Closed

[Merged by Bors] - refactor(LinearAlgebra/QuadraticForm): Replace BilinForm with a scalar valued bi LinearMap #10238

wants to merge 70 commits into from

Commits on Feb 1, 2024

  1. remove linMulLin

    @eric-wieser
    eric-wieser committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    eda1f6a View commit details
    Browse the repository at this point in the history

  2. other fixups

    @eric-wieser
    eric-wieser committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    9cc83ac View commit details
    Browse the repository at this point in the history

  3. fix

    @eric-wieser
    eric-wieser committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    9cd7289 View commit details
    Browse the repository at this point in the history

  4. Whitespace

    @eric-wieser
    eric-wieser committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    207098c View commit details
    Browse the repository at this point in the history

Commits on Feb 4, 2024

  1. Replace BilinForm with LinearMap

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

  2. CounterExample

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

  3. Lint

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

  4. Remove unused dependency

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

  5. Remove dependency on BilinForm from Basic

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

  6. LinearMap is now open

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

  7. Break out tensor product results

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

  8. Namespace LinearMap

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

  9. align

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

  10. Rename

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

  11. Rename

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

  12. Lint

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

  13. Update names in counter example

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

  14. Remove LinearMap

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

  15. Remove unnecessary stuff

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

  16. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

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

Commits on Feb 8, 2024

  1. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

    @mans0954
    mans0954 committed Feb 8, 2024
    Configuration menu
    Copy the full SHA
    c3f9c22 View commit details
    Browse the repository at this point in the history

  2. Fix

    @mans0954
    mans0954 committed Feb 8, 2024
    Configuration menu
    Copy the full SHA
    75f63e3 View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2024

  1. Define BilinForm.tensorDistrib in terms of LinearMap.tensorDistrib

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

  2. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

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

  3. Update Mathlib/LinearAlgebra/TensorProduct/LinearMap.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser committed Feb 11, 2024
    Configuration menu
    Copy the full SHA
    61a25f9 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/LinearAlgebra/TensorProduct/LinearMap.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser committed Feb 11, 2024
    Configuration menu
    Copy the full SHA
    5ad9864 View commit details
    Browse the repository at this point in the history

  5. Fix

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

  6. Move implementation notes

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

  7. Adjust ordering

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

  8. Add IsSymm.baseChange

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

  9. Port missing results to LinearAlgebra.TensorProduct.LinearMap

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

  10. Define BilinForm.tensorDistribEquiv in terms of LinearMap.tensorDistr… 

    …ibEquiv
    @mans0954
    mans0954 committed Feb 11, 2024
    Configuration menu
    Copy the full SHA
    9c9732e View commit details
    Browse the repository at this point in the history

  11. Prove BilinForm.IsSymm.tmul using LinearMap.IsSymm.tmul

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

  12. Fix simp

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

  13. Add TODO for bilinear map namespace

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

  14. Deduce BilinearForm/TensorProduct results from TensorProduct/LinearMap

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

  15. More progress

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

  16. Restore rfl proofs

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

  17. tensorDistribEquiv_toLinearMap

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

Commits on Feb 13, 2024

  1. Update docstring

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

  2. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

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

Commits on Feb 16, 2024

  1. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

    @mans0954
    mans0954 committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    8926c8e View commit details
    Browse the repository at this point in the history

  2. golf and docstrings

    @eric-wieser
    eric-wieser committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    ac85f43 View commit details
    Browse the repository at this point in the history

Commits on Feb 17, 2024

  1. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

    @mans0954
    mans0954 committed Feb 17, 2024
    Configuration menu
    Copy the full SHA
    0cbbdd8 View commit details
    Browse the repository at this point in the history

Commits on Feb 18, 2024

  1. Use new LinearMap.Bilinform

    @mans0954
    mans0954 committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    25a8d6d View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

    @mans0954
    mans0954 committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    201392e View commit details
    Browse the repository at this point in the history

  3. Update docstring

    @mans0954
    mans0954 committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    064bca4 View commit details
    Browse the repository at this point in the history

  4. Lint

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

  5. use open to further shrink the diff

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

  6. shrink the diff

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

  7. use the abbreviation

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

  8. Use LinearMap.BilinForm

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

  9. Fix

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

  10. Shrink diff

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

  11. Revert name polarBilin

    @mans0954
    mans0954 committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    47b4804 View commit details
    Browse the repository at this point in the history

  12. Save line

    @mans0954
    mans0954 committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    88a5298 View commit details
    Browse the repository at this point in the history

Commits on Feb 21, 2024

  1. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

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

  2. Fix

    @mans0954
    mans0954 committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    891d768 View commit details
    Browse the repository at this point in the history

  3. More use of LinearMap.BilinForm

    @mans0954
    mans0954 committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    031eb5c View commit details
    Browse the repository at this point in the history

  4. Much more LinearMap.BilinForm

    @mans0954
    mans0954 committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    1633049 View commit details
    Browse the repository at this point in the history

  5. Fix counterexamples

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

Commits on Feb 22, 2024

  1. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

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

  2. Fix

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

  3. Reduce diff

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

  4. Further reduce diff

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

Commits on Feb 23, 2024

  1. Update counter example

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

  2. Fix a few names

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

  3. Update docstrings

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

Commits on Feb 25, 2024

  1. reduce diff

    @eric-wieser
    eric-wieser committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    44d1d9e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into mans0954/quadratic-form-bilinear-map2

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