chore(algebra/group): rename as_monoid_hom into monoid_hom.of, define ring_hom.of (#1443)

* chore(algebra/group): rename `as_monoid_hom` into `monoid_hom.of`

This is similar to `Mon.of` etc.

* Fix compile

* Docs, missing universe

* Move variables declaration up as suggested by @jcommelin

* doc-string

Author: urkud

src/algebra/associated.lean

@@ -22,7 +22,7 @@ by rcases h with ⟨y, rfl⟩; exact is_unit_unit (units.map f y)
 
 lemma is_unit.map' [monoid α] [monoid β] (f : α → β) {x : α} (h : is_unit x) [is_monoid_hom f] :
   is_unit (f x) :=
-h.map (as_monoid_hom f)
+h.map (monoid_hom.of f)
 
 @[simp] theorem is_unit_zero_iff [semiring α] : is_unit (0 : α) ↔ (0:α) = 1 :=
 ⟨λ ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩, by rwa zero_mul at a0,

src/algebra/group/hom.lean

@@ -246,23 +246,22 @@ infixr ` →* `:25 := monoid_hom
 instance {M : Type*} {N : Type*} [monoid M] [monoid N] : has_coe_to_fun (M →* N) :=
 ⟨_, monoid_hom.to_fun⟩
 
-/-- Reinterpret a map `f : M → N` as a homomorphism `M →* N` -/
-@[to_additive as_add_monoid_hom]
-def as_monoid_hom {M : Type u} {N : Type v} [monoid M] [monoid N]
-  (f : M → N) [h : is_monoid_hom f] : M →* N :=
+
+namespace monoid_hom
+variables {M : Type*} {N : Type*} {P : Type*} [monoid M] [monoid N] [monoid P]
+variables {G : Type*} {H : Type*} [group G] [comm_group H]
+
+/-- Interpret a map `f : M → N` as a homomorphism `M →* N`. -/
+@[to_additive "Interpret a map `f : M → N` as a homomorphism `M →+ N`."]
+def of (f : M → N) [h : is_monoid_hom f] : M →* N :=
 { to_fun := f,
   map_one' := h.2,
   map_mul' := h.1.1 }
 
-@[simp, to_additive coe_as_add_monoid_hom]
-lemma coe_as_monoid_hom {M : Type u} {N : Type v} [monoid M] [monoid N]
-  (f : M → N) [is_monoid_hom f] : ⇑ (as_monoid_hom f) = f :=
+@[simp, to_additive]
+lemma coe_of (f : M → N) [is_monoid_hom f] : ⇑ (monoid_hom.of f) = f :=
 rfl
 
-namespace monoid_hom
-variables {M : Type*} {N : Type*} {P : Type*} [monoid M] [monoid N] [monoid P]
-variables {G : Type*} {H : Type*} [group G] [comm_group H]
-
 @[extensionality, to_additive]
 lemma ext ⦃f g : M →* N⦄ (h : (f : M → N) = g) : f = g :=
 by cases f; cases g; cases h; refl

src/algebra/group/units_hom.lean

@@ -19,8 +19,9 @@ monoid_hom.mk'
                   by rw [← f.map_mul, u.inv_val, f.map_one]⟩)
   (λ x y, ext (f.map_mul x y))
 
+/-- The group homomorphism on units induced by a multiplicative morphism. -/
 @[reducible] def map' (f : α → β) [is_monoid_hom f] : units α →* units β :=
-  map (as_monoid_hom f)
+  map (monoid_hom.of f)
 
 @[simp] lemma coe_map (f : α →* β) (x : units α) : ↑(map f x) = f x := rfl
 

src/algebra/ring.lean

@@ -322,17 +322,16 @@ instance {α : Type*} {β : Type*} [semiring α] [semiring β] : has_coe (α →
 
 namespace ring_hom
 
-/-- Construct a bundled `ring_hom` from a bare function and the appropriate typeclasses. -/
-def of {α : Type u} {β : Type v} [semiring α] [semiring β]
-  (f : α → β) [is_semiring_hom f] : α →+* β :=
+variables {β : Type v} {γ : Type w} [semiring α] [semiring β] [semiring γ]
+
+/-- Interpret `f : α → β` with `is_semiring_hom f` as a ring homomorphism. -/
+def of (f : α → β) [is_semiring_hom f] : α →+* β :=
 { to_fun := f,
-  .. as_monoid_hom f,
-  .. as_add_monoid_hom f }
+  .. monoid_hom.of f,
+  .. add_monoid_hom.of f }
 
-@[simp] lemma coe_of {α : Type u} {β : Type v} [semiring α] [semiring β]
-  (f : α → β) [is_semiring_hom f] : ⇑(of f) = f := rfl
+@[simp] lemma coe_of (f : α → β) [is_semiring_hom f] : ⇑(of f) = f := rfl
 
-variables {β : Type v} {γ : Type w} [semiring α] [semiring β] [semiring γ]
 variables (f : α →+* β) {x y : α}
 
 @[extensionality] theorem ext ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=