PR #2256 chore(data/equiv/basic): simp to_fun to coe

chore(data/equiv/basic): simp to_fun to coe #2256

mergify merged 8 commits into master from to_fun_as_coe

chore(data/equiv/basic): simp to_fun to coe

27140fd8

fix proofs

f2d9418a

jcommelin commented on 2020-03-27

urkud commented on 2020-03-27

kim-em commented on 2020-03-27

Update src/data/equiv/basic.lean

35e5658a

fix proof

f84cf7fa

Merge branch 'to_fun_as_coe' of github.com:leanprover-community/mathl…

24f78e5c

partially removing to_fun

78b06c0e

finish switching to coercions

1b6db585

kim-em added awaiting-review

jcommelin approved these changes on 2020-03-28

jcommelin removed awaiting-review

jcommelin added ready-to-merge

Merge branch 'master' into to_fun_as_coe

8a726cdd

mergify merged 17f83409 into master 5 years ago

bryangingechen deleted the to_fun_as_coe branch 5 years ago

Reviewers

jcommelin

gebner

urkud

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone