mathlib3
refactor(data/equiv/basic): simplify definition of equiv.set.range
#959
Merged

refactor(data/equiv/basic): simplify definition of equiv.set.range #959

mergify merged 3 commits into master from ChrisHughes24-patch-1
ChrisHughes24
ChrisHughes24 refactor(data/equiv/basic): simplify definition of equiv.set.range
c0b98f1c
ChrisHughes24 ChrisHughes24 requested a review 6 years ago
robertylewis
robertylewis commented on 2019-04-22
ChrisHughes24 delete duplicate
7fe4e708
robertylewis
robertylewis approved these changes on 2019-04-22
robertylewis robertylewis added ready-to-merge
Merge branch 'master' into 'ChrisHughes24-patch-1'
b42d9f0f
mergify mergify merged 45456cf1 into master 6 years ago
mergify mergify deleted the ChrisHughes24-patch-1 branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone