chore(algebra/group/units): use def to_units instead of has_lift (#1431)

* chore(algebra/group/units): use `def to_units` instead of `has_lift`

* Move, upgrade to `mul_equiv`, add documentation

Author: urkud

src/algebra/group/units.lean

@@ -149,10 +149,3 @@ theorem divp_mul_divp (x y : α) (ux uy : units α) :
 by rw [← divp_divp_eq_divp_mul, divp_assoc, mul_comm x, divp_assoc, mul_comm]
 
 end comm_monoid
-
-section group
-  variables [group α]
-
-  instance : has_lift α (units α) :=
-  ⟨λ a, ⟨a, a⁻¹, mul_inv_self _, inv_mul_self _⟩⟩
-end group

src/data/equiv/algebra.lean

@@ -304,6 +304,14 @@ instance is_group_hom {α β} [group α] [group β] (h : α ≃* β) :
 
 end mul_equiv
 
+/-- A group is isomorphic to its group of units. -/
+def to_units (α) [group α] : α ≃* units α :=
+{ to_fun := λ x, ⟨x, x⁻¹, mul_inv_self _, inv_mul_self _⟩,
+  inv_fun := coe,
+  left_inv := λ x, rfl,
+  right_inv := λ u, units.ext rfl,
+  map_mul' := λ x y, units.ext rfl }
+
 namespace units
 
 variables [monoid α] [monoid β] [monoid γ]