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] - chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop #2847

Closed
wants to merge 53 commits into from
Closed

[Merged by Bors] - chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop #2847

wants to merge 53 commits into from

Commits on May 28, 2020

  1. chore(algebra): displace zero_ne_one_class with nonzero

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    d1df178 View commit details
    Browse the repository at this point in the history

  2. algebra.ring

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    889420a View commit details
    Browse the repository at this point in the history

  3. Update src/algebra/ring.lean 

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

  4. update algebra.ring

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    8fc64cc View commit details
    Browse the repository at this point in the history

  5. algebra.group_with_zero

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    ba5497a View commit details
    Browse the repository at this point in the history

  6. algebra.group.with_one

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    4f7929c View commit details
    Browse the repository at this point in the history

  7. ring_theory.prod

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    3a0f538 View commit details
    Browse the repository at this point in the history

  8. algebra.field

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    217edd8 View commit details
    Browse the repository at this point in the history

  9. algebra.opposites

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    5fcca92 View commit details
    Browse the repository at this point in the history

  10. init_.data.int.basic

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    46b0420 View commit details
    Browse the repository at this point in the history

  11. algebra.ordered_ring

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    42f4d11 View commit details
    Browse the repository at this point in the history

  12. data.equiv.transfer_instances

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    24c18fb View commit details
    Browse the repository at this point in the history

  13. init_.data.nat.lemmas

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    ce14467 View commit details
    Browse the repository at this point in the history

  14. algebra.euclidean_domain

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    d34f6f2 View commit details
    Browse the repository at this point in the history

  15. data.equiv.ring

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    778c52d View commit details
    Browse the repository at this point in the history

  16. data.rat.basic

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    797c796 View commit details
    Browse the repository at this point in the history

  17. algebra.associated

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    16880d2 View commit details
    Browse the repository at this point in the history

  18. algebra.gcd_domain

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    953c707 View commit details
    Browse the repository at this point in the history

  19. data.zsqrtd.basic

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    7c51a9c View commit details
    Browse the repository at this point in the history

  20. set_theory.cardinal

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    1001e52 View commit details
    Browse the repository at this point in the history

  21. field_theory.subfield

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    1bfa31b View commit details
    Browse the repository at this point in the history

  22. ring_theory.fintype

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    a0d1d13 View commit details
    Browse the repository at this point in the history

  23. algebra.char_p

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    d3146b3 View commit details
    Browse the repository at this point in the history

  24. data.real.basic

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    09263be View commit details
    Browse the repository at this point in the history

  25. data.zmod.basic

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    e09e2ad View commit details
    Browse the repository at this point in the history

  26. data.real.nnreal

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    2f93b3e View commit details
    Browse the repository at this point in the history

  27. order.filter.filter_product

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    95897ff View commit details
    Browse the repository at this point in the history

  28. data.matrix.pequiv

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    821eb6c View commit details
    Browse the repository at this point in the history

  29. ring_theory.ideals

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    19f41df View commit details
    Browse the repository at this point in the history

  30. data.complex.exponential

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    acf8982 View commit details
    Browse the repository at this point in the history

  31. set_theory.ordinal

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    d4fe0eb View commit details
    Browse the repository at this point in the history

  32. linear_algebra.basis

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    27cd8a3 View commit details
    Browse the repository at this point in the history

  33. data.polynomial

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    f51a240 View commit details
    Browse the repository at this point in the history

  34. ring_theory.ideal_operations

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    4bacb83 View commit details
    Browse the repository at this point in the history

  35. ring_theory.noetherian

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    0b3ca61 View commit details
    Browse the repository at this point in the history

  36. data.padics.padic_integers

    @kckennylau
    kckennylau committed May 28, 2020
    Configuration menu
    Copy the full SHA
    b0a7e7e View commit details
    Browse the repository at this point in the history

Commits on May 29, 2020

  1. algebra.euclidean_domain

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    b1382b2 View commit details
    Browse the repository at this point in the history

  2. algebra.euclidean_domain: make more things protected

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    6110deb View commit details
    Browse the repository at this point in the history

  3. algebra.classical_lie_algebras

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    396edbf View commit details
    Browse the repository at this point in the history

  4. data.polynomial

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    b315a3e View commit details
    Browse the repository at this point in the history

  5. data.mv_polynomial

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    77b7f76 View commit details
    Browse the repository at this point in the history

  6. data.zsqrtd.gaussian_int

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    eb3fbe4 View commit details
    Browse the repository at this point in the history

  7. ring_theory.polynomial

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    da3bf8e View commit details
    Browse the repository at this point in the history

  8. ring_theory.free_comm_ring

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    3d96bc9 View commit details
    Browse the repository at this point in the history

  9. ring_theory.algebraic

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    94a474f View commit details
    Browse the repository at this point in the history

  10. algebra.direct_limit

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    a0a6e6f View commit details
    Browse the repository at this point in the history

  11. ring_theory.power_series

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    44db175 View commit details
    Browse the repository at this point in the history

  12. analysis.special_functions.pow

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    aa83f7f View commit details
    Browse the repository at this point in the history

  13. ring_theory.fractional_ideal

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    5f693c0 View commit details
    Browse the repository at this point in the history

  14. Merge remote-tracking branch 'origin/master' into nonzero

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    30ffafe View commit details
    Browse the repository at this point in the history

  15. fix errors

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    f7835fa View commit details
    Browse the repository at this point in the history

  16. it has gotten faster

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    ae3abc2 View commit details
    Browse the repository at this point in the history

  17. Merge branch 'master' into nonzero

    @kckennylau
    kckennylau committed May 29, 2020
    Configuration menu
    Copy the full SHA
    6fb14e9 View commit details
    Browse the repository at this point in the history