PR #12349 feat(*): fun_like instances on subtypes

feat(*): fun_like instances on subtypes #12349

dupuisf wants to merge 7 commits into master from dupuisf/subtype_fun_like

add fun_like stuff

fba265e7

embedding + algebra/group/hom

243ebd40

did a bunch more

079c3574

dupuisf added WIP

dupuisf added awaiting-CI

to_additive

1bf588fb

Vierkantor requested a review from

Vierkantor 3 years ago

Vierkantor commented on 2022-02-28

Update src/data/fun_like/basic.lean

4c95dd9c

fix lemma so it builds

16b210ea

ring_quot.lean

8a57cfd8

leanprover-community-bot-assistant added merge-conflict

kim-em added too-late

eric-wieser requested a review 2 years ago

Reviewers

Vierkantor

Assignees

No one assigned

Labels

WIP merge-conflict awaiting-CI too-late

Milestone

No milestone