PR #3770 feat(group/perm/sign): swap_adj_induction_on

feat(group/perm/sign): swap_adj_induction_on #3770

zhangir-azerbayev wants to merge 31 commits into master from algebra_multilinear_maps

feat(data/list/basic): Added Mario's lemma pmap_map

1c5955dd

added lemmas about permutations of fin n

e1325c6b

feat(linear_algebra/multilinear): added the multinear algebra_prod

b92773d6

feat(linear_algebra/alternating): made linear_algebra/alternating

52ee962e

feat(group_theory/units_action): added units actions

84a3ec59

feat(group_theory/perm/sign) added swap_induction_on'

1fbd7ea3

feat(group_theory/group_action: removed units action

abd3f202

feat(linear_algebra/alternating): added map_perm

ae37390f

feat(linear_algebra/alternating: added map_perm

1017e4e6

chore(linear_algebra/multilinear, linear_algebra/alternating): cleane…

d2801968

doc(linear_algebra/alternating): added documentation

a7a29e2e

zhangir-azerbayev requested a review from

kbuzzard 5 years ago

kim-em commented on 2020-08-14

kim-em added awaiting-author

style(linear_algebra/alternating): did reviewer suggestions for alter…

3f77cbe3

style(data/list/basic) did reviewer suggestions

9529e4d4

style(linear_algebra/multilinear): did reviewer suggestions

b2a8c932

jcommelin changed the title ~~Algebra multilinear maps~~ feat(linear_algebra): algebra multilinear maps 5 years ago

style(group_theory/perm/sign): reviewer suggestions

3fc73dbd

style(linear_algebra/multilinear): indenting

46ec7e74

style(linear_algebra/multilinear): more indenting

8cd80b5c

style(linear_algebra/multilinear: even more indenting

6bdeff4c

style(group_theory/perm/sign): more reviewer suggestions

873ec4e0

adamtopaz commented on 2020-08-14

feat(linear_algebra/alternating): semimodules over semirings

1827a5cd

fix(group_theory/perm/sign): removed unnecessary hypothesis from lemma

55fa7cca

fix(linear_algebra/alternating, linear_algebra/multilinear): fixed li…

4665cf59

zhangir-azerbayev removed review request from

kbuzzard 5 years ago

zhangir-azerbayev added awaiting-review

zhangir-azerbayev removed awaiting-author

Vierkantor requested a review from

Vierkantor 5 years ago

sgouezel commented on 2020-08-17

Vierkantor commented on 2020-08-17

Vierkantor removed awaiting-review

Vierkantor added awaiting-author

github-actions added merge-conflict

Merge remote-tracking branch 'origin/master' into algebra_multilinear…

0efa5f53

chore(*): Remove definitions which now exist elsewhere

ba169870

chore(*): Fix proof broken by updates to fin in core lean

8f7b07e7

chore(*): Fix linter error

97bac667

eric-wieser commented on 2020-11-23

github-actions removed merge-conflict

github-actions added merge-conflict

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

6aa9f5f0

chore(group_theory/perm/sign): Golf a proof

765613d9

github-actions removed merge-conflict

chore(group_theory/perm/sign): Golf another proof

ffbeb5f3

chore(group_theory/perm/sign): Golf another proof

eb5e3862

eric-wieser added WIP

github-actions added merge-conflict

Merge remote-tracking branch 'origin' into algebra_multilinear_maps

3ae70d98

github-actions removed merge-conflict

eric-wieser changed the title ~~feat(linear_algebra): algebra multilinear maps~~ feat(group/perm/sign): swap_adj_induction_on 5 years ago

github-actions added merge-conflict

github-actions removed merge-conflict

github-actions added merge-conflict

kim-em added too-late

Reviewers

eric-wieser

Vierkantor

sgouezel

kim-em

adamtopaz

Assignees

No one assigned

Labels

WIP awaiting-author merge-conflict too-late

Milestone

No milestone

mathlib3 feat(group/perm/sign): swap_adj_induction_on #3770 Open

feat(group/perm/sign): swap_adj_induction_on #3770

mathlib3
feat(group/perm/sign): swap_adj_induction_on
#3770

Open