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] - feat(linear_algebra/pi_tensor_product): define the tensor product of an indexed family of semimodules #5311

Closed
wants to merge 46 commits into from
Closed

[Merged by Bors] - feat(linear_algebra/pi_tensor_product): define the tensor product of an indexed family of semimodules #5311

wants to merge 46 commits into from

Commits on Dec 10, 2020

  1. add pi_tensor_product.lean

    @dupuisf
    dupuisf committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    205e946 View commit details
    Browse the repository at this point in the history

  2. some progress

    @dupuisf
    dupuisf committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    56ceca9 View commit details
    Browse the repository at this point in the history

  3. prove semimodule instance

    @dupuisf
    dupuisf committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    1016998 View commit details
    Browse the repository at this point in the history

  4. small changes

    @dupuisf
    dupuisf committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    c3db194 View commit details
    Browse the repository at this point in the history

  5. connection with multilinear maps, not finished

    @dupuisf
    dupuisf committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    2a5f055 View commit details
    Browse the repository at this point in the history

  6. documentation

    @dupuisf
    dupuisf committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    cb5d5f1 View commit details
    Browse the repository at this point in the history

  7. placate 100-char-per-line linter

    @dupuisf
    dupuisf committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    647e28a View commit details
    Browse the repository at this point in the history

  8. a few more todos

    @dupuisf
    dupuisf committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    c3d1d15 View commit details
    Browse the repository at this point in the history

  9. nonempty -> inhabited

    @dupuisf
    dupuisf committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    8243a2b View commit details
    Browse the repository at this point in the history

Commits on Dec 11, 2020

  1. add hidden R factor to deal with empty iota

    @dupuisf
    dupuisf committed Dec 11, 2020
    Configuration menu
    Copy the full SHA
    8157c3b View commit details
    Browse the repository at this point in the history

  2. prove semimodule instance for version with extra R

    @dupuisf
    dupuisf committed Dec 11, 2020
    Configuration menu
    Copy the full SHA
    d8da4a3 View commit details
    Browse the repository at this point in the history

  3. defined tprod in terms of tprod_coef

    @dupuisf
    dupuisf committed Dec 11, 2020
    Configuration menu
    Copy the full SHA
    b049492 View commit details
    Browse the repository at this point in the history

  4. now it compiles again

    @dupuisf
    dupuisf committed Dec 11, 2020
    Configuration menu
    Copy the full SHA
    fb9c0b9 View commit details
    Browse the repository at this point in the history

Commits on Dec 12, 2020

  1. 100 char linter

    @dupuisf
    dupuisf committed Dec 12, 2020
    Configuration menu
    Copy the full SHA
    d5337bc View commit details
    Browse the repository at this point in the history

  2. lemmas for ring case

    @dupuisf
    dupuisf committed Dec 12, 2020
    Configuration menu
    Copy the full SHA
    90f8af8 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into pi_tensor_product

    @dupuisf
    dupuisf committed Dec 12, 2020
    Configuration menu
    Copy the full SHA
    c1858fd View commit details
    Browse the repository at this point in the history

  4. add comment about requiring comm_ring

    @dupuisf
    dupuisf committed Dec 12, 2020
    Configuration menu
    Copy the full SHA
    3d721b6 View commit details
    Browse the repository at this point in the history

  5. define lift_add_hom to avoid this lift manually twice

    @dupuisf
    dupuisf committed Dec 12, 2020
    Configuration menu
    Copy the full SHA
    59a6a5e View commit details
    Browse the repository at this point in the history

Commits on Dec 13, 2020

  1. documentation

    @dupuisf
    dupuisf committed Dec 13, 2020
    Configuration menu
    Copy the full SHA
    0a44f0a View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2020

  1. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @dupuisf @jcommelin
    dupuisf and jcommelin committed Dec 16, 2020
    Configuration menu
    Copy the full SHA
    30a0893 View commit details
    Browse the repository at this point in the history

  2. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @dupuisf @jcommelin
    dupuisf and jcommelin committed Dec 16, 2020
    Configuration menu
    Copy the full SHA
    f4329df View commit details
    Browse the repository at this point in the history

  3. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @dupuisf @jcommelin
    dupuisf and jcommelin committed Dec 16, 2020
    Configuration menu
    Copy the full SHA
    f0d36d4 View commit details
    Browse the repository at this point in the history

  4. coef -> coeff

    @dupuisf
    dupuisf committed Dec 16, 2020
    Configuration menu
    Copy the full SHA
    aadfc8c View commit details
    Browse the repository at this point in the history

  5. 100 chars

    @dupuisf
    dupuisf committed Dec 16, 2020
    Configuration menu
    Copy the full SHA
    3a282cb View commit details
    Browse the repository at this point in the history

Commits on Dec 17, 2020

  1. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @dupuisf @eric-wieser
    dupuisf and eric-wieser committed Dec 17, 2020
    Configuration menu
    Copy the full SHA
    2c33be8 View commit details
    Browse the repository at this point in the history

  2. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @dupuisf @eric-wieser
    dupuisf and eric-wieser committed Dec 17, 2020
    Configuration menu
    Copy the full SHA
    a43a7a5 View commit details
    Browse the repository at this point in the history

  3. lift as an add_equiv

    @dupuisf
    dupuisf committed Dec 17, 2020
    Configuration menu
    Copy the full SHA
    687ff3e View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into pi_tensor_product

    @dupuisf
    dupuisf committed Dec 17, 2020
    Configuration menu
    Copy the full SHA
    3b90835 View commit details
    Browse the repository at this point in the history

  5. use map_neg

    @dupuisf
    dupuisf committed Dec 17, 2020
    Configuration menu
    Copy the full SHA
    84055b2 View commit details
    Browse the repository at this point in the history

Commits on Dec 18, 2020

  1. Merge together tprod and mk, and remove all the then-redundant lemmas

    @eric-wieser
    eric-wieser committed Dec 18, 2020
    Configuration menu
    Copy the full SHA
    88c1aa0 View commit details
    Browse the repository at this point in the history

  2. fix unused argument linter error in multilinear.lean

    @dupuisf
    dupuisf committed Dec 18, 2020
    Configuration menu
    Copy the full SHA
    9706bcd View commit details
    Browse the repository at this point in the history

  3. update module-level doc

    @dupuisf
    dupuisf committed Dec 18, 2020
    Configuration menu
    Copy the full SHA
    a92f5ad View commit details
    Browse the repository at this point in the history

  4. add warning against using tprod_coeff

    @dupuisf
    dupuisf committed Dec 18, 2020
    Configuration menu
    Copy the full SHA
    98e8545 View commit details
    Browse the repository at this point in the history

Commits on Dec 29, 2020

  1. Update src/linear_algebra/multilinear.lean 

    Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
    @dupuisf @kbuzzard
    dupuisf and kbuzzard committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    c75291e View commit details
    Browse the repository at this point in the history

  2. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
    @dupuisf @kbuzzard
    dupuisf and kbuzzard committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    90edfdd View commit details
    Browse the repository at this point in the history

  3. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
    @dupuisf @kbuzzard
    dupuisf and kbuzzard committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    f9542e5 View commit details
    Browse the repository at this point in the history

  4. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
    @dupuisf @kbuzzard
    dupuisf and kbuzzard committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    6d34517 View commit details
    Browse the repository at this point in the history

  5. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
    @dupuisf @kbuzzard
    dupuisf and kbuzzard committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    13f551a View commit details
    Browse the repository at this point in the history

  6. Update src/linear_algebra/pi_tensor_product.lean 

    Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
    @dupuisf @kbuzzard
    dupuisf and kbuzzard committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    6237a58 View commit details
    Browse the repository at this point in the history

  7. fix build + typo in docs

    @dupuisf
    dupuisf committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    9c76a0a View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' into pi_tensor_product

    @dupuisf
    dupuisf committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    b8b192a View commit details
    Browse the repository at this point in the history

  9. scalar tower

    @dupuisf
    dupuisf committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    7b3be80 View commit details
    Browse the repository at this point in the history

  10. fix

    @dupuisf
    dupuisf committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    c261010 View commit details
    Browse the repository at this point in the history

  11. linter

    @dupuisf
    dupuisf committed Dec 29, 2020
    Configuration menu
    Copy the full SHA
    5e3fa95 View commit details
    Browse the repository at this point in the history

Commits on Jan 3, 2021

  1. Merge branch 'master' into pi_tensor_product

    @dupuisf
    dupuisf committed Jan 3, 2021
    Configuration menu
    Copy the full SHA
    1b8ef90 View commit details
    Browse the repository at this point in the history

Commits on Jan 7, 2021

  1. delete useless smul_zero lemma

    @dupuisf
    dupuisf committed Jan 7, 2021
    Configuration menu
    Copy the full SHA
    d140385 View commit details
    Browse the repository at this point in the history