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(data/set_like): remove repeated boilerplate from subobjects #6768

Closed
wants to merge 80 commits into from
Closed

[Merged by Bors] - feat(data/set_like): remove repeated boilerplate from subobjects #6768

wants to merge 80 commits into from

Commits on Mar 19, 2021

  1. feat(data/set_like): remove repeated boilerplate from subobjects

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    25763e9 View commit details
    Browse the repository at this point in the history

  2. fix

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    3152def View commit details
    Browse the repository at this point in the history

  3. remove more code

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    caaa0eb View commit details
    Browse the repository at this point in the history

  4. fix

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    b805524 View commit details
    Browse the repository at this point in the history

  5. add docs

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    4e8fc3c View commit details
    Browse the repository at this point in the history

  6. fix

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    3b2e1a1 View commit details
    Browse the repository at this point in the history

  7. fix

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    edd817f View commit details
    Browse the repository at this point in the history

  8. fix

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    c224de8 View commit details
    Browse the repository at this point in the history

  9. fix

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    cced824 View commit details
    Browse the repository at this point in the history

  10. fix

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    62846b3 View commit details
    Browse the repository at this point in the history

  11. Update src/group_theory/group_action/sub_mul_action.lean

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    d2c8620 View commit details
    Browse the repository at this point in the history

  12. Remove more duplicates

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    e052900 View commit details
    Browse the repository at this point in the history

  13. fix

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    1a180c7 View commit details
    Browse the repository at this point in the history

  14. Remove bits of subalgebra too

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    b6fec94 View commit details
    Browse the repository at this point in the history

  15. Fix more lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    8f301d7 View commit details
    Browse the repository at this point in the history

  16. Fix more lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    9990015 View commit details
    Browse the repository at this point in the history

  17. lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    79a8774 View commit details
    Browse the repository at this point in the history

  18. lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    7e47baf View commit details
    Browse the repository at this point in the history

  19. lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    be26aa9 View commit details
    Browse the repository at this point in the history

  20. lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    f97c6f9 View commit details
    Browse the repository at this point in the history

  21. lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    b28ba31 View commit details
    Browse the repository at this point in the history

  22. lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    0a37b81 View commit details
    Browse the repository at this point in the history

  23. lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    00d6447 View commit details
    Browse the repository at this point in the history

  24. lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    bbbf002 View commit details
    Browse the repository at this point in the history

  25. lemma renames

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    60e826d View commit details
    Browse the repository at this point in the history

  26. Tidy up

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    639cfae View commit details
    Browse the repository at this point in the history

  27. Merge remote-tracking branch 'origin/master' into eric-wieser/has_inj… 

    …ective_coe_set

# Conflicts:
#	src/linear_algebra/basic.lean
    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    4d5621c View commit details
    Browse the repository at this point in the history

  28. fix implicitness

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    50d5dac View commit details
    Browse the repository at this point in the history

  29. tidy subfield too

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    bb24547 View commit details
    Browse the repository at this point in the history

  30. fix

    @eric-wieser
    eric-wieser committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    f2328e3 View commit details
    Browse the repository at this point in the history

Commits on Mar 20, 2021

  1. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    5229e6c View commit details
    Browse the repository at this point in the history

  2. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    bf5c4ec View commit details
    Browse the repository at this point in the history

  3. Convert intermediate_field

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    ff1bd74 View commit details
    Browse the repository at this point in the history

  4. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    1132bd9 View commit details
    Browse the repository at this point in the history

  5. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    203f3e3 View commit details
    Browse the repository at this point in the history

  6. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    1d46d25 View commit details
    Browse the repository at this point in the history

  7. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    293ba5d View commit details
    Browse the repository at this point in the history

  8. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    a13577b View commit details
    Browse the repository at this point in the history

  9. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    990ac3c View commit details
    Browse the repository at this point in the history

  10. chore(ring_theory/adjoin/basic): golf some proofs about algebra.adjoin

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    9201c8d View commit details
    Browse the repository at this point in the history

  11. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    1aef6c8 View commit details
    Browse the repository at this point in the history

  12. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    5919cb0 View commit details
    Browse the repository at this point in the history

  13. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    46e1ef2 View commit details
    Browse the repository at this point in the history

  14. remove a coercion

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    b45ecbb View commit details
    Browse the repository at this point in the history

  15. remove the other coe too

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    eb37101 View commit details
    Browse the repository at this point in the history

  16. cleanup coercions

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    7c69e92 View commit details
    Browse the repository at this point in the history

  17. fix adjoin/basic

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    d220305 View commit details
    Browse the repository at this point in the history

  18. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    283b5e6 View commit details
    Browse the repository at this point in the history

  19. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    7460b13 View commit details
    Browse the repository at this point in the history

  20. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    c37c73e View commit details
    Browse the repository at this point in the history

  21. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    b397a23 View commit details
    Browse the repository at this point in the history

  22. add missing coercion lemmas

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    2e4ede4 View commit details
    Browse the repository at this point in the history

  23. more simp lemmas

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    b55b582 View commit details
    Browse the repository at this point in the history

  24. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    2753823 View commit details
    Browse the repository at this point in the history

  25. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    1c3af59 View commit details
    Browse the repository at this point in the history

  26. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    8971ff7 View commit details
    Browse the repository at this point in the history

  27. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    0bcfb61 View commit details
    Browse the repository at this point in the history

  28. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    3250cec View commit details
    Browse the repository at this point in the history

  29. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    c3af803 View commit details
    Browse the repository at this point in the history

  30. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    b5f87dc View commit details
    Browse the repository at this point in the history

  31. fix

    @eric-wieser
    eric-wieser committed Mar 20, 2021
    Configuration menu
    Copy the full SHA
    67bef56 View commit details
    Browse the repository at this point in the history

Commits on Mar 24, 2021

  1. Merge branch 'master' of github.com:leanprover-community/mathlib into… 

    … eric-wieser/has_injective_coe_set

# Conflicts:
#	src/algebra/algebra/subalgebra.lean
#	src/field_theory/splitting_field.lean
#	src/ring_theory/adjoin/basic.lean
    @eric-wieser
    eric-wieser committed Mar 24, 2021
    Configuration menu
    Copy the full SHA
    6430902 View commit details
    Browse the repository at this point in the history

  2. fix

    @eric-wieser
    eric-wieser committed Mar 24, 2021
    Configuration menu
    Copy the full SHA
    3175682 View commit details
    Browse the repository at this point in the history

  3. Update src/topology/algebra/continuous_functions.lean

    @eric-wieser
    eric-wieser committed Mar 24, 2021
    Configuration menu
    Copy the full SHA
    918747c View commit details
    Browse the repository at this point in the history

  4. fix

    @eric-wieser
    eric-wieser committed Mar 24, 2021
    Configuration menu
    Copy the full SHA
    5b8c9a5 View commit details
    Browse the repository at this point in the history

  5. Update adjoin.lean

    @eric-wieser
    eric-wieser committed Mar 24, 2021
    Configuration menu
    Copy the full SHA
    453defa View commit details
    Browse the repository at this point in the history

Commits on Mar 25, 2021

  1. fix

    @eric-wieser
    eric-wieser committed Mar 25, 2021
    Configuration menu
    Copy the full SHA
    8832e45 View commit details
    Browse the repository at this point in the history

  2. fix

    @eric-wieser
    eric-wieser committed Mar 25, 2021
    Configuration menu
    Copy the full SHA
    ecb8dd4 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into eric-wieser/has_injective_coe_set

    @eric-wieser
    eric-wieser committed Mar 25, 2021
    Configuration menu
    Copy the full SHA
    1ae10af View commit details
    Browse the repository at this point in the history

  4. Add back removed instances

    @eric-wieser
    eric-wieser committed Mar 25, 2021
    Configuration menu
    Copy the full SHA
    294592c View commit details
    Browse the repository at this point in the history

  5. placate the linter

    @eric-wieser
    eric-wieser committed Mar 25, 2021
    Configuration menu
    Copy the full SHA
    0d2413c View commit details
    Browse the repository at this point in the history

  6. Merge branch 'eric-wieser/has_injective_coe_set' of github.com:leanpr… 

    …over-community/mathlib into eric-wieser/has_injective_coe_set
    @eric-wieser
    eric-wieser committed Mar 25, 2021
    Configuration menu
    Copy the full SHA
    8949414 View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2021

  1. lintfix

    @eric-wieser
    eric-wieser committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    edc52b6 View commit details
    Browse the repository at this point in the history

  2. sort imports 

    Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
    @eric-wieser @Vierkantor
    eric-wieser and Vierkantor committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    2bef33c View commit details
    Browse the repository at this point in the history

  3. make the argument implicit again

    @eric-wieser
    eric-wieser committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    0eae887 View commit details
    Browse the repository at this point in the history

Commits on Mar 28, 2021

  1. Merge branch 'master' of github.com:leanprover-community/mathlib into… 

    … eric-wieser/has_injective_coe_set
    @eric-wieser
    eric-wieser committed Mar 28, 2021
    Configuration menu
    Copy the full SHA
    5ff2867 View commit details
    Browse the repository at this point in the history

Commits on Mar 29, 2021

  1. Fix error introduced by merge

    @eric-wieser
    eric-wieser committed Mar 29, 2021
    Configuration menu
    Copy the full SHA
    6c42c31 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of github.com:leanprover-community/mathlib into… 

    … eric-wieser/has_injective_coe_set
    @eric-wieser
    eric-wieser committed Mar 29, 2021
    Configuration menu
    Copy the full SHA
    8da99bd View commit details
    Browse the repository at this point in the history

  3. more fixes

    @eric-wieser
    eric-wieser committed Mar 29, 2021
    Configuration menu
    Copy the full SHA
    0163276 View commit details
    Browse the repository at this point in the history

Commits on Mar 30, 2021

  1. fix

    @eric-wieser
    eric-wieser committed Mar 30, 2021
    Configuration menu
    Copy the full SHA
    36d2531 View commit details
    Browse the repository at this point in the history