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

[Merged by Bors] - feat(group_theory/perm/basic): Bundle sigma_congr_right and sum_congr into monoid_homs #5301

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(group_theory/perm/basic): Bundle sigma_congr_right and sum_congr into monoid_homs #5301

wants to merge 4 commits into from

Commits on Dec 10, 2020

  1. feat(gruop_theory/perm/basic): Bundle sigma_congr_right and sum_congr… 

    … into monoid_homs
    @eric-wieser
    eric-wieser committed Dec 10, 2020
    Configuration menu
    Copy the full SHA
    a450e0d View commit details
    Browse the repository at this point in the history

Commits on Dec 15, 2020

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

    … eric-wieser/perm-homs
    @eric-wieser
    eric-wieser committed Dec 15, 2020
    Configuration menu
    Copy the full SHA
    a2fef88 View commit details
    Browse the repository at this point in the history

  2. feat(group_theory/perm/basic): Remove subgroup definitions, add `fint… 

    …ype.card` theorems
    @eric-wieser
    eric-wieser committed Dec 15, 2020
    Configuration menu
    Copy the full SHA
    fe9d21d View commit details
    Browse the repository at this point in the history

  3. chore(*): Golf proof

    @eric-wieser
    eric-wieser committed Dec 15, 2020
    Configuration menu
    Copy the full SHA
    fe9cee2 View commit details
    Browse the repository at this point in the history