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.

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

[Merged by Bors] - feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and similar typeclasses #9511

Closed
wants to merge 43 commits into from

Commits on Jan 5, 2024

  1. feat(Algebra/Ring/Ext): start writing ext lemmas for rings

    This is based on discussion in the Zulip thread
    https://leanprover.zulipchat.com/stream/287929-mathlib4/topic/Ring.20is.20determined.20by.20Semiring.
    
    Note that this commit introduce `sorry`s into the codebase. It is a WIP.
    raghuram-13 committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    294d9c6 View commit details
    Browse the repository at this point in the history

Commits on Jan 6, 2024

  1. Configuration menu
    Copy the full SHA
    432b6c0 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    a9f6a29 View commit details
    Browse the repository at this point in the history
  3. feat(Algebra/Ring/Ext): prove extensionality lemmas for Semiring

    Prove `Semiring.ext` and `Semiring.ext_iff` lemmas, as well as that
    `Semiring.toNonUnitalSemiring` and `Semiring.toNonAssocSemiring` are
    injective.
    raghuram-13 committed Jan 6, 2024
    Configuration menu
    Copy the full SHA
    a849abc View commit details
    Browse the repository at this point in the history
  4. refactor(Algebra/Ring/Ext): restructure ext lemmas for Semiring

    Prove the injectivity lemma in terms of the `ext` lemma, as the former
    goes through showing that `h_add` and `h_mul` hold anyway.
    raghuram-13 committed Jan 6, 2024
    Configuration menu
    Copy the full SHA
    0182195 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    a9d2b96 View commit details
    Browse the repository at this point in the history
  6. feat(Algebra/Ring/Ext): add injectivity lemma for NonAssocSemiring

    Prove that `NonAssocSemiring.toNonUnitalNonAssocSemiring` is
    injective.
    raghuram-13 committed Jan 6, 2024
    Configuration menu
    Copy the full SHA
    c6683f4 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    60dc1a1 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    200fc5c View commit details
    Browse the repository at this point in the history
  9. feat(Algebra/Ring/Ext): prove ext lemmas for NonUnitalNonAssocRing

    Prove an `ext` lemma and use it to show that
    `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` is injective as
    well as an `ext_iff` lemma.
    raghuram-13 committed Jan 6, 2024
    Configuration menu
    Copy the full SHA
    c99d235 View commit details
    Browse the repository at this point in the history
  10. feat(Algebra/Ring/Ext): add injectivity lemma for `NonUnitalNonAssocS…

    …emiring`
    
    Show that `NonUnitalNonAssocSemiring.toDistrib` is injective.
    raghuram-13 committed Jan 6, 2024
    Configuration menu
    Copy the full SHA
    c138be4 View commit details
    Browse the repository at this point in the history
  11. style(Algebra/Ring/Ext): remove unused names, change rcases to cases

    One exception: leave the `h` in `fun h ↦` in `ext_iff` proofs,
    for (marginally) more readability.
    raghuram-13 committed Jan 6, 2024
    Configuration menu
    Copy the full SHA
    505d31d View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    e32510d View commit details
    Browse the repository at this point in the history
  13. feat(Algebra/Ring/Ext): add injectivity lemma for Semiring

    Prove that `Semiring.toNonAssocSemiring` is injective.
    raghuram-13 committed Jan 6, 2024
    Configuration menu
    Copy the full SHA
    7a4fcce View commit details
    Browse the repository at this point in the history
  14. feat(Algebra/Ring/Ext): start ext lemmas for {NonUnital,NonAssoc,}Ring

    For each of the three typeclasses, state the `ext` lemma with a
    sorried proof and prove the consequences (injectivity and `ext_iff`
    lemmas).
    raghuram-13 committed Jan 6, 2024
    Configuration menu
    Copy the full SHA
    db29b79 View commit details
    Browse the repository at this point in the history
  15. Configuration menu
    Copy the full SHA
    4b40300 View commit details
    Browse the repository at this point in the history
  16. Configuration menu
    Copy the full SHA
    6178024 View commit details
    Browse the repository at this point in the history
  17. style(Algebra/Ring/Ext): add some inline comments

    Highlight the locations in the file where something mathematically
    non-trivial is proved: namely that some operation is determined by
    others. (There are essentially only two such.)
    raghuram-13 committed Jan 6, 2024
    Configuration menu
    Copy the full SHA
    e5e5486 View commit details
    Browse the repository at this point in the history
  18. Configuration menu
    Copy the full SHA
    70282a3 View commit details
    Browse the repository at this point in the history
  19. Configuration menu
    Copy the full SHA
    4b2249e View commit details
    Browse the repository at this point in the history
  20. Configuration menu
    Copy the full SHA
    993a7f3 View commit details
    Browse the repository at this point in the history

Commits on Jan 7, 2024

  1. Configuration menu
    Copy the full SHA
    c78ee2a View commit details
    Browse the repository at this point in the history
  2. style(Algebra/Ring/Ext): change variable names

    Change `a`, `b` to `x`, `y` in accordance with
    https://leanprover-community.github.io/contribute/style.html#variable-conventions.
    
    Additionally, remove an unnecessary `'` from a variable `inst`.
    raghuram-13 committed Jan 7, 2024
    Configuration menu
    Copy the full SHA
    9412010 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    af0f907 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    7d24100 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    c36ab27 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    41329f7 View commit details
    Browse the repository at this point in the history

Commits on Jan 9, 2024

  1. doc(Algebra/Ring/Ext): fix copyright year

    Realise that it is now 2024 :).
    
    Co-authored-by: Riccardo Brasca <[email protected]>
    raghuram-13 and riccardobrasca authored Jan 9, 2024
    Configuration menu
    Copy the full SHA
    0b335dd View commit details
    Browse the repository at this point in the history
  2. doc(Algebra/Ring/Ext): fix typo

    Fix typo in module header describing file.
    
    Co-authored-by: Eric Wieser <[email protected]>
    raghuram-13 and eric-wieser authored Jan 9, 2024
    Configuration menu
    Copy the full SHA
    2c5b5f8 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2024

  1. Configuration menu
    Copy the full SHA
    b0a10f3 View commit details
    Browse the repository at this point in the history
  2. style(Algebra/Ring/Ext): change format for referring to other files

    This is in accordance with the discussion in the thread
    #9511 (comment).
    raghuram-13 committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    10abca9 View commit details
    Browse the repository at this point in the history
  3. feat(Algebra/Ring/Ext): extract some further extensionality lemmas

    Leave the `Add(Comm)MonoidWithOne` and `Add(Comm)GroupWithOne`
    extensionality lemmas in `Mathlib/Algebra/Ring/Ext.lean` for now.
    
    This resolves comments #9511 (comment)
    and #9511 (comment).
    raghuram-13 committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    309b6ed View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    ce97567 View commit details
    Browse the repository at this point in the history

Commits on Apr 8, 2024

  1. Configuration menu
    Copy the full SHA
    50fa902 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    6580ed5 View commit details
    Browse the repository at this point in the history
  3. refactor(Algebra/Ring/Ext): change macro to "point-free" style

    WARNING: this commit is NOT error-free.
    raghuram-13 committed Apr 8, 2024
    Configuration menu
    Copy the full SHA
    f081164 View commit details
    Browse the repository at this point in the history
  4. refactor(Algebra/Ring/Ext): change ext lemma arguments to new style

    WARNING: this commit is NOT error-free.
    raghuram-13 committed Apr 8, 2024
    Configuration menu
    Copy the full SHA
    bddf5fa View commit details
    Browse the repository at this point in the history
  5. refactor(Algebra/Ring/Ext): change ext_iff arguments to new style

    WARNING: this commit is NOT error-free.
    raghuram-13 committed Apr 8, 2024
    Configuration menu
    Copy the full SHA
    6eca4f8 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    fbee3e7 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    35b590c View commit details
    Browse the repository at this point in the history

Commits on May 9, 2024

  1. Configuration menu
    Copy the full SHA
    8ceebd8 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    d096e0b View commit details
    Browse the repository at this point in the history
  3. fix(Algebra/Ring/Ext): fix error caused by upstream changes.

    Specifically, replace `← Int.coe_nat_eq` with `Int.ofNat_eq_coe`.
    raghuram-13 committed May 9, 2024
    Configuration menu
    Copy the full SHA
    d410631 View commit details
    Browse the repository at this point in the history