Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-15 05:08 e48ad0dc

View on Github →

chore(*): migrate units.map to bundled homs (#1331)

Estimated changes

added def units.coe_hom
added theorem units.coe_hom_apply
added theorem units.coe_map'
modified theorem units.coe_map
added def units.map'
added def units.map
modified theorem units.map_comp
modified theorem units.map_id