PR #2204 feat(data/equiv): pi_congr

feat(data/equiv): pi_congr #2204

mergify merged 11 commits into master from equiv.pi_congr

feat(data/equiv): pi_congr

0ce88626

docstrings

beeb1f52

change case for consistency

732b0ec3

tidying up

120219bd

switching names

3d86aa49

kim-em added awaiting-review

kim-em requested a review from

digama0 6 years ago

fixes

1577c622

cipher1024 assigned

digama0 6 years ago

robertylewis commented on 2020-03-24

Update src/data/equiv/basic.lean

5e863797

implicit arguments

999fd41f

Merge remote-tracking branch 'origin/master' into equiv.pi_congr

28fa982f

robertylewis approved these changes on 2020-03-25

robertylewis removed awaiting-review

robertylewis added ready-to-merge

Merge branch 'master' into equiv.pi_congr

85ddc0b8

Merge branch 'master' into equiv.pi_congr

6c0d0222

mergify merged 1eae0be1 into master 6 years ago

robertylewis deleted the equiv.pi_congr branch 6 years ago

Reviewers

robertylewis

digama0

Assignees

digama0

Labels

ready-to-merge

Milestone

No milestone