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

feat(LinearAlgebra/DirectSum/Finsupp) : tensor products of finsupp functions #10824

Closed
wants to merge 68 commits into from
Closed

feat(LinearAlgebra/DirectSum/Finsupp) : tensor products of finsupp functions #10824

wants to merge 68 commits into from

Commits on Feb 21, 2024

  1. generalize to CommSemiring / AddCommMonoid

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    d8e50fc View commit details
    Browse the repository at this point in the history

  2. generalize to CommSemiring / AddCommMonoid

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    fa4cb7e View commit details
    Browse the repository at this point in the history

  3. add finsupp_sum_tmul and 3 variants

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    53ee15d View commit details
    Browse the repository at this point in the history

  4. revert

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    d55ac1e View commit details
    Browse the repository at this point in the history

  5. rename (temp)

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    2f1ebe7 View commit details
    Browse the repository at this point in the history

  6. something working

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    c28b2e6 View commit details
    Browse the repository at this point in the history

  7. lint 100

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    2320a61 View commit details
    Browse the repository at this point in the history

  8. revert the generalization (-> AddCommGroup/CommSemiring in the initia… 

    …l file)
    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    1fdd0aa View commit details
    Browse the repository at this point in the history

  9. rename following EW's suggestion

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    d76a5a9 View commit details
    Browse the repository at this point in the history

  10. namespace TensorProduct

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    423a61d View commit details
    Browse the repository at this point in the history

  11. add docstring

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    2efdc69 View commit details
    Browse the repository at this point in the history

  12. update Mathlib.lean

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    98b197b View commit details
    Browse the repository at this point in the history

  13. update Mathlib.lean

    Antoine Chambert-Loir committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    7f13321 View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2024

  1. better inferface for polynomial (via finsuppScalarLeft)

    Antoine Chambert-Loir committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    aa3eaf6 View commit details
    Browse the repository at this point in the history

  2. add letI in RingTheory/Flat/Basic

    Antoine Chambert-Loir committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    3e12239 View commit details
    Browse the repository at this point in the history

  3. adjust simp to make Lie/TensorProduct compile

    Antoine Chambert-Loir committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    8458d4e View commit details
    Browse the repository at this point in the history

  4. remove useless import

    Antoine Chambert-Loir committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    e259731 View commit details
    Browse the repository at this point in the history

Commits on Feb 23, 2024

  1. Merge branch 'master' into ACL/FinsuppTensorProd

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

  2. re-add variable

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    19af3b0 View commit details
    Browse the repository at this point in the history

  3. remove multiplicativity (doesn't work yet)

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    d26f775 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/LinearAlgebra/DirectSum/Finsupp.lean 

    Change i to iota

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
    @AntoineChambert-Loir @alreadydone
    AntoineChambert-Loir and alreadydone committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    660e471 View commit details
    Browse the repository at this point in the history

  5. add finsuppScalarRight

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    65e6c20 View commit details
    Browse the repository at this point in the history

  6. add TensorProduct of MonoidAlgebra

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    a7b0441 View commit details
    Browse the repository at this point in the history

  7. add docstring

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    8af8487 View commit details
    Browse the repository at this point in the history

  8. add docstrings for definitions

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    4f65f96 View commit details
    Browse the repository at this point in the history

  9. lint100

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    b1742d9 View commit details
    Browse the repository at this point in the history

  10. update Mathlib.lean

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    85b2839 View commit details
    Browse the repository at this point in the history

  11. add "todo" note

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    3fb1a0a View commit details
    Browse the repository at this point in the history

Commits on Feb 24, 2024

  1. do the construction in the other directions (using AlgebraTensorProduct)

    Antoine Chambert-Loir committed Feb 24, 2024
    Configuration menu
    Copy the full SHA
    c375537 View commit details
    Browse the repository at this point in the history

  2. small progress

    Antoine Chambert-Loir committed Feb 24, 2024
    Configuration menu
    Copy the full SHA
    e296050 View commit details
    Browse the repository at this point in the history

  3. delete garbage

    Antoine Chambert-Loir committed Feb 24, 2024
    Configuration menu
    Copy the full SHA
    ef9a571 View commit details
    Browse the repository at this point in the history

  4. remove bad "end"

    Antoine Chambert-Loir committed Feb 24, 2024
    Configuration menu
    Copy the full SHA
    6c74740 View commit details
    Browse the repository at this point in the history

  5. Algebra for MvPolynomial

    Antoine Chambert-Loir committed Feb 24, 2024
    Configuration menu
    Copy the full SHA
    d9ce8e2 View commit details
    Browse the repository at this point in the history

Commits on Feb 25, 2024

  1. cleanup

    Antoine Chambert-Loir committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    ec42703 View commit details
    Browse the repository at this point in the history

  2. cleanup

    Antoine Chambert-Loir committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    d7c43b0 View commit details
    Browse the repository at this point in the history

  3. move files

    Antoine Chambert-Loir committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    32d9c2e View commit details
    Browse the repository at this point in the history

  4. adjust Mathlib.lean

    Antoine Chambert-Loir committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    417d963 View commit details
    Browse the repository at this point in the history

  5. equiv for polynomial

    Antoine Chambert-Loir committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    337b52a View commit details
    Browse the repository at this point in the history

  6. shorten some lines; review-dog

    Antoine Chambert-Loir committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    5a5f1a9 View commit details
    Browse the repository at this point in the history

  7. linter 100

    Antoine Chambert-Loir committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    cdc4ef9 View commit details
    Browse the repository at this point in the history

  8. dedup namespace

    Antoine Chambert-Loir committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    5112ca4 View commit details
    Browse the repository at this point in the history

Commits on Feb 29, 2024

  1. Merge branch 'master' into ACL/FinsuppTensorProd

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    47a6c00 View commit details
    Browse the repository at this point in the history

  2. Do what review dog suggests 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @AntoineChambert-Loir @github-actions
    AntoineChambert-Loir and github-actions[bot] committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    746bb43 View commit details
    Browse the repository at this point in the history

  3. generalize Monoid to MulOneClass

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    20c8b2d View commit details
    Browse the repository at this point in the history

  4. add docstrings

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    1665702 View commit details
    Browse the repository at this point in the history

  5. add docstrings

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    f0a5d8b View commit details
    Browse the repository at this point in the history

  6. one more doctring

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    fc8f0d1 View commit details
    Browse the repository at this point in the history

  7. yet another docstring

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    0e751b9 View commit details
    Browse the repository at this point in the history

  8. docstring : change i to iota (3 lines)

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    d3ade35 View commit details
    Browse the repository at this point in the history

  9. lint 100

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    87d6d87 View commit details
    Browse the repository at this point in the history

  10. remove unused equiv

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    cdfd7b1 View commit details
    Browse the repository at this point in the history

Commits on Mar 13, 2024

  1. Merge branch 'master' into ACL/FinsuppTensorProd

    Antoine Chambert-Loir committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    91c0278 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Algebra/Lie/TensorProduct.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @AntoineChambert-Loir @github-actions
    AntoineChambert-Loir and github-actions[bot] committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    c2496b2 View commit details
    Browse the repository at this point in the history

  3. change import in 3 files

    Antoine Chambert-Loir committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    02e19a6 View commit details
    Browse the repository at this point in the history

  4. correct badly formed import line

    Antoine Chambert-Loir committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    073c214 View commit details
    Browse the repository at this point in the history

  5. import lines were still wrong…

    Antoine Chambert-Loir committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    47be110 View commit details
    Browse the repository at this point in the history

  6. that should be good…

    Antoine Chambert-Loir committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    119763f View commit details
    Browse the repository at this point in the history

Commits on Mar 21, 2024

  1. generalize one universe

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    c16067f View commit details
    Browse the repository at this point in the history

  2. add MvPolynomial.lcoeff

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    845bb95 View commit details
    Browse the repository at this point in the history

  3. add lemmas

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    8004cfc View commit details
    Browse the repository at this point in the history

  4. indent correctly

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    de94570 View commit details
    Browse the repository at this point in the history

  5. correct the unfinished proof

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    cfa238f View commit details
    Browse the repository at this point in the history

Commits on Apr 9, 2024

  1. Merge branch 'master' into ACL/FinsuppTensorProd

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    aa4b9a4 View commit details
    Browse the repository at this point in the history

  2. adjust MvPolynomial to merged version of finsupptensorprod

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    f3d3ee2 View commit details
    Browse the repository at this point in the history

  3. mv two lemmas to Data/Finsupp

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    df63d70 View commit details
    Browse the repository at this point in the history

  4. add explicit arguments

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    8d31f5d View commit details
    Browse the repository at this point in the history

Commits on Apr 10, 2024

  1. Replace noisy simp?

    @ocfnash
    ocfnash committed Apr 10, 2024
    Configuration menu
    Copy the full SHA
    f1719b8 View commit details
    Browse the repository at this point in the history

Commits on Apr 11, 2024

  1. Merge branch 'master' into ACL/FinsuppTensorProd

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Apr 11, 2024
    Configuration menu
    Copy the full SHA
    c724436 View commit details
    Browse the repository at this point in the history