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/invariant_basis_number): strong_rank_condition_iff_succ #9128

Closed
wants to merge 58 commits into from
Closed

[Merged by Bors] - feat(linear_algebra/invariant_basis_number): strong_rank_condition_iff_succ #9128

wants to merge 58 commits into from

Commits on Sep 10, 2021

  1. add natural inclusion

    @riccardobrasca
    riccardobrasca committed Sep 10, 2021
    Configuration menu
    Copy the full SHA
    fddf261 View commit details
    Browse the repository at this point in the history

  2. add strong_rank_condition_iff

    @riccardobrasca
    riccardobrasca committed Sep 10, 2021
    Configuration menu
    Copy the full SHA
    a060a97 View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2021

  1. Update src/linear_algebra/free_module.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    8d45d54 View commit details
    Browse the repository at this point in the history

  2. Update src/linear_algebra/invariant_basis_number.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    40d5808 View commit details
    Browse the repository at this point in the history

  3. Update src/linear_algebra/invariant_basis_number.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    d12acbe View commit details
    Browse the repository at this point in the history

  4. Update src/linear_algebra/free_module.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    a243479 View commit details
    Browse the repository at this point in the history

  5. Update src/linear_algebra/free_module.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    f3f9c6f View commit details
    Browse the repository at this point in the history

  6. fix build

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    e4d46f8 View commit details
    Browse the repository at this point in the history

  7. add exten_by_one

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    2a23f2d View commit details
    Browse the repository at this point in the history

  8. dd extend_apply' and extend_injective

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    9a38685 View commit details
    Browse the repository at this point in the history

  9. golf

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    7e994e8 View commit details
    Browse the repository at this point in the history

  10. add extend_by_one_of_one

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    3492dad View commit details
    Browse the repository at this point in the history

  11. golf

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    7f9a2a2 View commit details
    Browse the repository at this point in the history

  12. add extend_by_one_mul

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    badec8b View commit details
    Browse the repository at this point in the history

  13. fix build

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    b0f1290 View commit details
    Browse the repository at this point in the history

  14. fix name

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    6f2a436 View commit details
    Browse the repository at this point in the history

  15. better nam

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    6de73e6 View commit details
    Browse the repository at this point in the history

  16. add pi.extend_by_zero.linear_map

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    e9dce92 View commit details
    Browse the repository at this point in the history

  17. useless

    @riccardobrasca
    riccardobrasca committed Sep 13, 2021
    Configuration menu
    Copy the full SHA
    f99046c View commit details
    Browse the repository at this point in the history

Commits on Sep 14, 2021

  1. fix build

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    4e6787b View commit details
    Browse the repository at this point in the history

  2. doc

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    8e2fa86 View commit details
    Browse the repository at this point in the history

  3. typo

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    f9616cd View commit details
    Browse the repository at this point in the history

  4. typo

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    9fbaac8 View commit details
    Browse the repository at this point in the history

  5. No commit message

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    ea62a08 View commit details
    Browse the repository at this point in the history

  6. golf

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    6202578 View commit details
    Browse the repository at this point in the history

  7. fix build

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    4aa99a8 View commit details
    Browse the repository at this point in the history

  8. golf

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    7e97dc8 View commit details
    Browse the repository at this point in the history

  9. add lemmas

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    3348b86 View commit details
    Browse the repository at this point in the history

  10. add function.extend_smul

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    1991d09 View commit details
    Browse the repository at this point in the history

  11. fix build

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    fc8204f View commit details
    Browse the repository at this point in the history

  12. fix name

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    32470ae View commit details
    Browse the repository at this point in the history

  13. doc

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    aac5986 View commit details
    Browse the repository at this point in the history

  14. fix name autogenerated

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    a0c4688 View commit details
    Browse the repository at this point in the history

  15. fix build

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    68c2500 View commit details
    Browse the repository at this point in the history

  16. fix build

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    58a0a53 View commit details
    Browse the repository at this point in the history

  17. explicit variable

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    97b0570 View commit details
    Browse the repository at this point in the history

  18. fix build

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    747e766 View commit details
    Browse the repository at this point in the history

  19. fix build

    @riccardobrasca
    riccardobrasca committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    1137194 View commit details
    Browse the repository at this point in the history

Commits on Sep 15, 2021

  1. unused argument

    @riccardobrasca
    riccardobrasca committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    2729c91 View commit details
    Browse the repository at this point in the history

  2. fix build

    @riccardobrasca
    riccardobrasca committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    e8f373d View commit details
    Browse the repository at this point in the history

  3. Update src/linear_algebra/invariant_basis_number.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    3570fdd View commit details
    Browse the repository at this point in the history

  4. add @[mk_iff] to strong_rank_condition

    @riccardobrasca
    riccardobrasca committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    7ca0a75 View commit details
    Browse the repository at this point in the history

  5. Update src/linear_algebra/pi.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    3b6bd12 View commit details
    Browse the repository at this point in the history

  6. Update src/linear_algebra/pi.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    ad69679 View commit details
    Browse the repository at this point in the history

  7. Update src/algebra/group/pi.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    ed4d589 View commit details
    Browse the repository at this point in the history

  8. better name

    @riccardobrasca
    riccardobrasca committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    7fe1d6a View commit details
    Browse the repository at this point in the history

  9. reorganize a section

    @riccardobrasca
    riccardobrasca committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    d6a07dd View commit details
    Browse the repository at this point in the history

  10. Update src/linear_algebra/pi.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @riccardobrasca @eric-wieser
    riccardobrasca and eric-wieser committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    368bcdd View commit details
    Browse the repository at this point in the history

  11. golf

    @riccardobrasca
    riccardobrasca committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    65ae338 View commit details
    Browse the repository at this point in the history

  12. fix build

    @riccardobrasca
    riccardobrasca committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    61fbe55 View commit details
    Browse the repository at this point in the history

  13. fix build

    @riccardobrasca
    riccardobrasca committed Sep 15, 2021
    Configuration menu
    Copy the full SHA
    36e15b3 View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2021

  1. Merge branch 'master' into strong_rank_iff

    @riccardobrasca
    riccardobrasca committed Sep 16, 2021
    Configuration menu
    Copy the full SHA
    c5e5f2e View commit details
    Browse the repository at this point in the history

  2. cyclic import

    @riccardobrasca
    riccardobrasca committed Sep 16, 2021
    Configuration menu
    Copy the full SHA
    f15908a View commit details
    Browse the repository at this point in the history

Commits on Sep 18, 2021

  1. move lemma

    @riccardobrasca
    riccardobrasca committed Sep 18, 2021
    1 Configuration menu
    Copy the full SHA
    7eedf41 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into strong_rank_iff

    @riccardobrasca
    riccardobrasca committed Sep 18, 2021
    Configuration menu
    Copy the full SHA
    33ccb51 View commit details
    Browse the repository at this point in the history

  3. golf

    @riccardobrasca
    riccardobrasca committed Sep 18, 2021
    Configuration menu
    Copy the full SHA
    3fa9b8b View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2021

  1. Merge branch 'master' into strong_rank_iff

    @riccardobrasca
    riccardobrasca committed Sep 21, 2021
    Configuration menu
    Copy the full SHA
    2b04535 View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2021

  1. Merge branch 'master' into strong_rank_iff

    @riccardobrasca
    riccardobrasca committed Sep 23, 2021
    Configuration menu
    Copy the full SHA
    e7b0c91 View commit details
    Browse the repository at this point in the history