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

Modified src/algebra/associated.lean

added theorem is_unit.map'

added theorem is_unit.map

added theorem is_unit.mk0

Modified src/algebra/group/hom.lean

added def as_monoid_hom

added theorem coe_as_monoid_hom

Modified src/algebra/group/units_hom.lean

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

Modified src/data/equiv/algebra.lean

Modified src/data/polynomial.lean

Modified src/field_theory/splitting_field.lean

Modified src/ring_theory/localization.lean

Modified src/ring_theory/power_series.lean