Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added ideal_inter_nonempty, proved that a maximal ideal is prime #6924

Closed
wants to merge 73 commits into from
Closed

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added ideal_inter_nonempty, proved that a maximal ideal is prime #6924

wants to merge 73 commits into from

Commits on Mar 12, 2021

  1. feat(order/ideal) added is_prime and is_maximal ideals

    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    367ba3a View commit details
    Browse the repository at this point in the history

  2. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    fa268b1 View commit details
    Browse the repository at this point in the history

  3. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    ad910d6 View commit details
    Browse the repository at this point in the history

  4. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    79b765d View commit details
    Browse the repository at this point in the history

  5. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    4d2b2da View commit details
    Browse the repository at this point in the history

  6. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    0ff4f09 View commit details
    Browse the repository at this point in the history

  7. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    6e472a5 View commit details
    Browse the repository at this point in the history

  8. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    c6d2b3d View commit details
    Browse the repository at this point in the history

  9. starting to work on is_prime_of_is_maximal

    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    ae380c3 View commit details
    Browse the repository at this point in the history

  10. Update ideal.lean

    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    663f793 View commit details
    Browse the repository at this point in the history

  11. Merge remote-tracking branch 'refs/remotes/origin/prime_ideal' into p… 

    …rime_ideal
    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    d6076c7 View commit details
    Browse the repository at this point in the history

  12. Merge branch 'prime_ideal' of github.com:leanprover-community/mathlib… 

    … into prime_ideal
    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    3e76e40 View commit details
    Browse the repository at this point in the history

  13. Update ideal.lean

    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    3217ff6 View commit details
    Browse the repository at this point in the history

  14. fixed bugs

    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    2be706e View commit details
    Browse the repository at this point in the history

  15. Merge remote-tracking branch 'refs/remotes/origin/prime_ideal' into p… 

    …rime_ideal
    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    9cd7320 View commit details
    Browse the repository at this point in the history

  16. Update ideal.lean

    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    e0c3590 View commit details
    Browse the repository at this point in the history

  17. Update ideal.lean

    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    7cb44dc View commit details
    Browse the repository at this point in the history

  18. removed prime_of_is_maximal

    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    f6a3300 View commit details
    Browse the repository at this point in the history

  19. Merge branch 'prime_ideal' of github.com:leanprover-community/mathlib… 

    … into prime_ideal
    @atarnoam
    atarnoam committed Mar 12, 2021
    Configuration menu
    Copy the full SHA
    2d337d8 View commit details
    Browse the repository at this point in the history

Commits on Mar 13, 2021

  1. Update src/order/ideal.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    ed01b5f View commit details
    Browse the repository at this point in the history

  2. Made the lattice instance of I more general. 

    To show that `ideal P` is a lattice, it now suffices
to check that `P` has joins
and that the
intersection of any two ideals is nonempty.

Also added an equivalent
characteristic of the join ideal
when `P` is a lattice.
    @atarnoam
    atarnoam committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    8c597f1 View commit details
    Browse the repository at this point in the history

  3. Changed proper to is_proper

    @atarnoam
    atarnoam committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    472ebac View commit details
    Browse the repository at this point in the history

  4. Merge branch 'prime_ideal' of github.com:leanprover-community/mathlib… 

    … into prime_ideal
    @atarnoam
    atarnoam committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    e63fe2b View commit details
    Browse the repository at this point in the history

  5. is_prime, is_maximal now extend is_proper.

    @atarnoam
    atarnoam committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    926c4ed View commit details
    Browse the repository at this point in the history

  6. made is_maximal and is_prime to typeclasses.

    @atarnoam
    atarnoam committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    8fc4dcf View commit details
    Browse the repository at this point in the history

  7. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    1d1dbfe View commit details
    Browse the repository at this point in the history

  8. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    6bab0df View commit details
    Browse the repository at this point in the history

  9. added is_ideal, is_filter, prime_pair

    @atarnoam
    atarnoam committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    7813092 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'prime_ideal' into is_prime_of_is_maximal

    @atarnoam
    atarnoam committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    e3a09e8 View commit details
    Browse the repository at this point in the history

  11. Update prime_ideal.lean

    @atarnoam
    atarnoam committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    52ae523 View commit details
    Browse the repository at this point in the history

  12. If I is prime, x \inf y \in I, 

     then `x \in I` or `y \in I`
    @atarnoam
    atarnoam committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    3abbe48 View commit details
    Browse the repository at this point in the history

Commits on Mar 15, 2021

  1. Update src/order/pfilter.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    c9ac5c4 View commit details
    Browse the repository at this point in the history

  2. Update src/order/pfilter.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    4974ff1 View commit details
    Browse the repository at this point in the history

  3. Update src/order/pfilter.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    a3c2c0c View commit details
    Browse the repository at this point in the history

  4. Update src/order/pfilter.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    89257a7 View commit details
    Browse the repository at this point in the history

  5. Update src/order/prime_ideal.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    7a70b0d View commit details
    Browse the repository at this point in the history

  6. Update src/order/ideal.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    dc4dca8 View commit details
    Browse the repository at this point in the history

  7. Update src/order/prime_ideal.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    e0a1b83 View commit details
    Browse the repository at this point in the history

  8. Update src/order/prime_ideal.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    23907a7 View commit details
    Browse the repository at this point in the history

  9. Update src/order/prime_ideal.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    f175e85 View commit details
    Browse the repository at this point in the history

  10. Update src/order/prime_ideal.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    9663a56 View commit details
    Browse the repository at this point in the history

  11. Update pfilter.lean

    @atarnoam
    atarnoam committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    9c591ca View commit details
    Browse the repository at this point in the history

Commits on Mar 16, 2021

  1. Update src/order/ideal.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Mar 16, 2021
    Configuration menu
    Copy the full SHA
    f611e16 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @mguaypaq @bryangingechen
    3 people committed Mar 16, 2021
    Configuration menu
    Copy the full SHA
    3bda7c6 View commit details
    Browse the repository at this point in the history

Commits on Mar 20, 2021

  1. Merge remote-tracking branch 'community/master' into prime_ideal

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    619ea26 View commit details
    Browse the repository at this point in the history

  2. fix, style tweaks

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    3e2f540 View commit details
    Browse the repository at this point in the history

  3. add order.pfilter.is_prime

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    a0beea8 View commit details
    Browse the repository at this point in the history

  4. Update src/order/prime_ideal.lean

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    604475c View commit details
    Browse the repository at this point in the history

  5. use compl in prime_pair

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    26954c4 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'community/prime_ideal' into prime_ideal

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    cb8b1d6 View commit details
    Browse the repository at this point in the history

  7. Update src/order/pfilter.lean

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    18e5500 View commit details
    Browse the repository at this point in the history

  8. naming

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    0d0cf5a View commit details
    Browse the repository at this point in the history

  9. disjoint, cover

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    feaa40b View commit details
    Browse the repository at this point in the history

  10. use is_compl in prime_pair

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    ccf25f2 View commit details
    Browse the repository at this point in the history

  11. golf

    @bryangingechen
    bryangingechen committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    255a361 View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2021

  1. Merge branch 'prime_ideal' into is_prime_of_is_maximal

    @atarnoam
    atarnoam committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    9e9e67d View commit details
    Browse the repository at this point in the history

Commits on Mar 28, 2021

  1. proved that a maximal ideal is prime

    @atarnoam
    atarnoam committed Mar 28, 2021
    Configuration menu
    Copy the full SHA
    0a4cea2 View commit details
    Browse the repository at this point in the history

  2. Added documentation

    @atarnoam
    atarnoam committed Mar 28, 2021
    Configuration menu
    Copy the full SHA
    52ec220 View commit details
    Browse the repository at this point in the history

  3. set lower priority

    @atarnoam
    atarnoam committed Mar 28, 2021
    Configuration menu
    Copy the full SHA
    e38c4b5 View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2021

  1. Merge branch 'master' into is_prime_of_is_maximal

    @atarnoam
    atarnoam committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    fafe945 View commit details
    Browse the repository at this point in the history

  2. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    561095a View commit details
    Browse the repository at this point in the history

  3. Update src/order/pfilter.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    8bf9cd4 View commit details
    Browse the repository at this point in the history

  4. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    2bfd823 View commit details
    Browse the repository at this point in the history

  5. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    7e79f24 View commit details
    Browse the repository at this point in the history

  6. Update src/order/ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    e9e4544 View commit details
    Browse the repository at this point in the history

  7. Update src/order/prime_ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    4b79c1a View commit details
    Browse the repository at this point in the history

  8. Update src/order/prime_ideal.lean 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @atarnoam @bryangingechen
    atarnoam and bryangingechen committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    8a1f2bc View commit details
    Browse the repository at this point in the history

  9. removed attribute simp from mem_def

    @atarnoam
    atarnoam committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    ee19aee View commit details
    Browse the repository at this point in the history

Commits on Apr 8, 2021

  1. Update src/order/ideal.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @atarnoam @jcommelin
    atarnoam and jcommelin committed Apr 8, 2021
    Configuration menu
    Copy the full SHA
    1d2bf9b View commit details
    Browse the repository at this point in the history

  2. changed mem_def to mem_coe

    @atarnoam
    atarnoam committed Apr 8, 2021
    Configuration menu
    Copy the full SHA
    667a4a2 View commit details
    Browse the repository at this point in the history

Commits on Apr 11, 2021

  1. applied CR

    @atarnoam
    atarnoam committed Apr 11, 2021
    Configuration menu
    Copy the full SHA
    06ac08d View commit details
    Browse the repository at this point in the history

  2. applied CR

    @atarnoam
    atarnoam committed Apr 11, 2021
    Configuration menu
    Copy the full SHA
    a028592 View commit details
    Browse the repository at this point in the history

Commits on Apr 14, 2021

  1. Update src/order/ideal.lean 

    Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>
    @atarnoam @mguaypaq
    atarnoam and mguaypaq committed Apr 14, 2021
    Configuration menu
    Copy the full SHA
    b91a965 View commit details
    Browse the repository at this point in the history