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

refactor(LinearAlgebra/BilinearForm/TensorProduct): Tensor products of bilinear maps #14988

Open
wants to merge 66 commits into
base: master
Choose a base branch
from
Open

refactor(LinearAlgebra/BilinearForm/TensorProduct): Tensor products of bilinear maps #14988

wants to merge 66 commits into from
+144 −60

Commits on Jul 21, 2024

  1. Make LinearMap.BilinMap.tensorDistrib work for bilinear maps

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

  2. Progress

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

  3. Get LinearAlgebra/BilinearForm/TensorProduct to build by commenting s… 

    …tuff out
    @mans0954
    mans0954 committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    7f4b8b4 View commit details
    Browse the repository at this point in the history

  4. Get LinearAlgebra/QuadraticForm/TensorProduct to build by commenting … 

    …stuff out
    @mans0954
    mans0954 committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    3dcc169 View commit details
    Browse the repository at this point in the history

  5. Fix

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

  6. Add more N

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

Commits on Jul 22, 2024

  1. Recover BilinForm

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

  2. Tidy uo

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

  3. Just try to get it building

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

  4. Mostly put it back together

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

  5. Reorg

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

  6. fudge it into building

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

Commits on Jul 23, 2024

  1. Implement LinearMap.BilinMap.congr₂ with LinearEquiv.congrRight

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

  2. Implement LinearMap.BilinForm.congr with LinearEquiv.congrRight and L… 

    …inearEquiv.congrLeft
    @mans0954
    mans0954 committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    624ba77 View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

Commits on Aug 1, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

Commits on Aug 7, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

Commits on Aug 9, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

Commits on Aug 15, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

    @mans0954
    mans0954 committed Aug 15, 2024
    Configuration menu
    Copy the full SHA
    03a4d93 View commit details
    Browse the repository at this point in the history

  2. Remove unused vars

    @mans0954
    mans0954 committed Aug 15, 2024
    Configuration menu
    Copy the full SHA
    35779ab View commit details
    Browse the repository at this point in the history

Commits on Aug 23, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

Commits on Aug 31, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

    @mans0954
    mans0954 committed Aug 31, 2024
    Configuration menu
    Copy the full SHA
    b1c3526 View commit details
    Browse the repository at this point in the history

Commits on Sep 7, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

Commits on Sep 13, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

Commits on Sep 20, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

    @mans0954
    mans0954 committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    cdf6efc View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2024

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

    Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
    @mans0954 @erdOne
    mans0954 and erdOne authored Oct 2, 2024
    Configuration menu
    Copy the full SHA
    32fae52 View commit details
    Browse the repository at this point in the history

  2. Correct doc string

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

  3. Remove spurious --

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

  4. Merge branch 'master' into mans0954/tensorDistrib

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

Commits on Oct 3, 2024

  1. Add docstrings

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

Commits on Oct 5, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

  2. deprecate and change name

    @eric-wieser
    eric-wieser committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    390c528 View commit details
    Browse the repository at this point in the history

  3. Fix

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

  4. QuadraticMap.congr₂

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

  5. LinearMap.BilinMap.congr₂

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

  6. congr₂_refl and congr₂_symm

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

  7. Rename

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

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

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @mans0954 @github-actions
    mans0954 and github-actions[bot] authored Oct 5, 2024
    Configuration menu
    Copy the full SHA
    02c2c5a View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2024

  1. Add congr₂ section

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

  2. tidy

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

  3. fix double-namespace

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

  4. Merge branch 'mans0954/congr₂' into mans0954/tensorDistrib

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

Commits on Oct 14, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

  2. Fix

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

  3. Gah

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

Commits on Oct 24, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

  2. Remove duplicate def

    @mans0954
    mans0954 committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    4133bb3 View commit details
    Browse the repository at this point in the history

  3. Dot notation

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

Commits on Oct 25, 2024

  1. Update Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean 

    Co-authored-by: Eric Wieser <efw@google.com>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser authored Oct 25, 2024
    Configuration menu
    Copy the full SHA
    cd7de90 View commit details
    Browse the repository at this point in the history

  2. Rename

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

  3. Merge branch 'master' into mans0954/tensorDistrib

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

  4. Remove old docstring

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

  5. Remove old docstring

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

  6. Update comment

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

  7. Fix

    @mans0954
    mans0954 committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    1677ddc View commit details
    Browse the repository at this point in the history

  8. Simplify

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

Commits on Oct 26, 2024

  1. Update Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean 

    Co-authored-by: Eric Wieser <efw@google.com>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser authored Oct 26, 2024
    Configuration menu
    Copy the full SHA
    7823fa3 View commit details
    Browse the repository at this point in the history

  2. Try new QuadraticForm.tensorDistrib def

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

  3. Patch it back together

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

  4. Remove unused argument

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

  5. Improve

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

  6. Remove alternative def

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

  7. BilinMap versions of baseChange and baseChange_tmul

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

Commits on Oct 27, 2024

  1. Merge branch 'master' into mans0954/tensorDistrib

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

Commits on Oct 28, 2024

  1. Add explanitory note

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

  2. Move comment

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