mathlib3
feat(group_theory/perm/sign): Add lemma about (sigma_congr_right σ).sign
#5923
Open
Open
feat(group_theory/perm/sign): Add lemma about (sigma_congr_right σ).sign #5923
eric-wieser
wants to merge
22 commits into
master
from
eric-wieser/sigma_congr_right_sign
chore(group_theory/perm): Add alternate formulation of (sum|sigma)_co…
b88abe98
chore(data/equiv/basic): Add lemmas about sum_congr and swap
a9d434a9
feat(group_theory/perm/sign): Add sign_sum_congr
66ef6e2f
chore(group_theory/perm/sign): Tidy the proof
7528d8d9
Add lemmas about sigma_congr
d122c550
wip
405d27bd
chore(algebra/group/pi): Split into multiple files
2916a9fb
chore(algebra/group/pi): Split into multiple files
5f7f155a
chore(algebra/group/pi): Split into multiple files
e337f687
Merge branch 'eric-wieser/split-pi' into eric-wieser/sigma_congr_righ…
c142ad77
Tidy lemmas
8b139016
Finish the proof except for an "obvious" sorry
3246375b
Merge remote-tracking branch 'origin/master' into eric-wieser/sigma_c…
b8c75dd7
Merge remote-tracking branch 'origin' into eric-wieser/sigma_congr_ri…
282b195b
Add missing bundled homs
1f0cbc81
Merge remote-tracking branch 'origin' into eric-wieser/sigma_congr_ri…
4efa5baa
fix(*): Remove duplicate definition
988e494d
remove duplicate lemma
88f141c2
Merge branch 'master' into eric-wieser/sigma_congr_right_sign
5091f0be
Merge remote-tracking branch 'origin/master' into eric-wieser/sigma_c…
607b3393
fix
bb30acbb
progress?
995c1ac0
Reviewers
No reviews
Assignees
No one assigned
Labels
WIP
incomplete
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub