units): add units.coe_mk_of_mul_eq_one
#1938

Merged

feat(algebra/group/units): add units.coe_mk_of_mul_eq_one #1938

mergify merged 1 commit into master from jcommelin-patch-4-1

Update units.lean

7e190d3c

ChrisHughes24 approved these changes on 2020-02-01

ChrisHughes24 added ready-to-merge

mergify merged a500c24c into master 6 years ago

mergify deleted the jcommelin-patch-4-1 branch 6 years ago

Reviewers

ChrisHughes24

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone