mathlib3
chore(linear_map): use curly brackets for type class in linear_map coe_to_fun
#1493

Merged

chore(linear_map): use curly brackets for type class in linear_map coe_to_fun #1493

mergify merged 3 commits into master from linear_map_coe

chore(linear_map): use curly brackets for type class in linear_map co…

213cbd4a

fix

1b2af256

ChrisHughes24 requested a review 6 years ago

ChrisHughes24 changed the title ~~Linear map coe~~ chore(linear_map): use curly brackets for type class in linear_map coe_to_fun 6 years ago

jcommelin approved these changes on 2019-10-01

jcommelin added ready-to-merge

Merge branch 'master' into linear_map_coe

231ed6c6

mergify merged 800dba4f into master 6 years ago

mergify deleted the linear_map_coe branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone