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(group_theory): use generic subobject_class lemmas #11758

Closed
wants to merge 55 commits into from
Closed

[Merged by Bors] - feat(group_theory): use generic subobject_class lemmas #11758

wants to merge 55 commits into from

Commits on Apr 8, 2022

  1. chore(group_theory): replace subobject.op_mem lemmas with generic ones

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    157cf1a View commit details
    Browse the repository at this point in the history

  2. Further protect the op_mem lemmas in subclasses of the op_mem_class

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    4c165e8 View commit details
    Browse the repository at this point in the history

  3. Fix algebra/pointwise.lean (parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    28b7944 View commit details
    Browse the repository at this point in the history

  4. Fix algebra/module/submodule_lattice.lean (param changes)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    0b442a0 View commit details
    Browse the repository at this point in the history

  5. Fix data/dfinsupp/basic.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    256b8c2 View commit details
    Browse the repository at this point in the history

  6. Fix data/dfinsupp/basic.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    2bb5035 View commit details
    Browse the repository at this point in the history

  7. Fix linear_algebra/basic.lean (mostly changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    d76cb01 View commit details
    Browse the repository at this point in the history

  8. Fix linear_algebra/quotient.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    cccf471 View commit details
    Browse the repository at this point in the history

  9. Fix linear_algebra/finsupp.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    719045f View commit details
    Browse the repository at this point in the history

  10. Fix algebra/algebra/basic.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    4f7d2bf View commit details
    Browse the repository at this point in the history

  11. Fix algebra/algebra/operations.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    cd2317d View commit details
    Browse the repository at this point in the history

  12. Fix algebra/algebra/tower.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    4d5128d View commit details
    Browse the repository at this point in the history

  13. Fix linear_algebra/linear_independent.lean (changed parameters, squ… 

    …eeze simp)
    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    9ae821a View commit details
    Browse the repository at this point in the history

  14. Fix ring_theory/principal_ideal_domain.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    6c7eafc View commit details
    Browse the repository at this point in the history

  15. Fix ring_theory/polynomial/scale_roots.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    f2b2116 View commit details
    Browse the repository at this point in the history

  16. Fix linear_algebra/std_basis.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    7ed3c16 View commit details
    Browse the repository at this point in the history

  17. Fix ring_theory/adjoin.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    3911598 View commit details
    Browse the repository at this point in the history

  18. Fix ring_theory/algebra_tower.lean (changed parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    67ee2b6 View commit details
    Browse the repository at this point in the history

  19. Fix linear_algebra/finite_dimensional.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    43fe8ec View commit details
    Browse the repository at this point in the history

  20. Fix field_theory/finite/polynomial.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    aa6e502 View commit details
    Browse the repository at this point in the history

  21. Fix analysis/convex/basic (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    b5f2579 View commit details
    Browse the repository at this point in the history

  22. Fix field_theory/primitive_element.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    e199dbe View commit details
    Browse the repository at this point in the history

  23. Fix field_theory/abel_ruffini.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    4b4305a View commit details
    Browse the repository at this point in the history

  24. Fix analysis/inner_product_space/l2_space.lean (parameters)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    7e8ca44 View commit details
    Browse the repository at this point in the history

  25. Fix (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    9bd4403 View commit details
    Browse the repository at this point in the history

  26. Fix ring_theory/subring/basic.lean (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    e77885a View commit details
    Browse the repository at this point in the history

  27. Fix ring_theory/subring/basic.lean (move stuff to the right section)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    4d72196 View commit details
    Browse the repository at this point in the history

  28. Lint fix

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    c6f15f7 View commit details
    Browse the repository at this point in the history

  29. Fix algebra/star/unitary.lean (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    4094ede View commit details
    Browse the repository at this point in the history

  30. Fix deprecated/subgroup.lean (disambiguate overloads)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    9a99124 View commit details
    Browse the repository at this point in the history

  31. Fix data/finupp/basic.lean (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    74d4c11 View commit details
    Browse the repository at this point in the history

  32. Fix algebra/module/submodule.lean (params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    4361982 View commit details
    Browse the repository at this point in the history

  33. Fix data/dfinsupp/basic.lean (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    b27f625 View commit details
    Browse the repository at this point in the history

  34. Fix linear_algebra/linear_pmap.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    e6aff27 View commit details
    Browse the repository at this point in the history

  35. Fix linear_algebra/linear_pmap.lean (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    1cdef7a View commit details
    Browse the repository at this point in the history

  36. Fix linear_algebra/linear_independent.lean (help elaborator)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    75817b6 View commit details
    Browse the repository at this point in the history

  37. Fix linear_algebra/dfinsupp.lean (genericize lemmas)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    d71ab03 View commit details
    Browse the repository at this point in the history

  38. Update algebra/algebra/operations.lean

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    81d6a38 View commit details
    Browse the repository at this point in the history

  39. Fix algebra/algebra/subalgebra.lean (use solve_by_elim instead of… 

    … `try { apply }`)
    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    5d98bf1 View commit details
    Browse the repository at this point in the history

  40. Fix duplicate instance

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    86ef9a2 View commit details
    Browse the repository at this point in the history

  41. Fix algebra/direct_sum/internal.lean (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    b5ef481 View commit details
    Browse the repository at this point in the history

  42. Fix ring_theory/integral_closure.lean (changed params, genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    53bfe68 View commit details
    Browse the repository at this point in the history

  43. Fix field_theory/intermediate_field.lean (delete duplicate lemmas)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    03dd0ba View commit details
    Browse the repository at this point in the history

  44. Fix ring_theory/local_properties.lean (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    c681e34 View commit details
    Browse the repository at this point in the history

  45. Fix algebra/lie/cartan_subalgebra.lean (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    3a14e40 View commit details
    Browse the repository at this point in the history

  46. Fix analysis/convex/cone.lean (genericize)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    04f14ca View commit details
    Browse the repository at this point in the history

  47. Fix ring_theory/ideal/basic.lean (protect more lemmas)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    c937535 View commit details
    Browse the repository at this point in the history

  48. Fix ring_theory/jacobson_ideal.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    62b261c View commit details
    Browse the repository at this point in the history

  49. Fix modifications to pow_mem in `group_theory/submonoid/membership.… 

    …lean`
    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    4c9bc9f View commit details
    Browse the repository at this point in the history

  50. Fix algebra/module/submodule.lean (duplicate instances)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    5cfedd8 View commit details
    Browse the repository at this point in the history

  51. Fix linear_algebra/span.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    9bda6d1 View commit details
    Browse the repository at this point in the history

  52. Fix linear_algebra/prod.lean (changed params)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    0159ea9 View commit details
    Browse the repository at this point in the history

  53. Fix algebra/algebra/subalgebra/basic.lean (remove duplicate lemma)

    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    01a5008 View commit details
    Browse the repository at this point in the history

  54. Fix algebra/algebra/subalgebra/pointwise.lean (changed param, type … 

    …ascript the coercion between subalgebra and submodule)
    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    42afb41 View commit details
    Browse the repository at this point in the history

  55. Fix ring_theory/graded_algebra/homogeneous_localization.lean (chang… 

    …ed params)
    @Vierkantor
    Vierkantor committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    e764eef View commit details
    Browse the repository at this point in the history