has_map_add.lean

set_option old_structure_cmd true

class has_coe_to_fun' (Γ dom cod : Type) :=
( to_fun : Γ → dom → cod )

instance has_coe_to_fun'.has_coe_to_fun (Γ α β : Type) [has_coe_to_fun' Γ α β] : 
  has_coe_to_fun Γ := ⟨_, @has_coe_to_fun'.to_fun _ α β _⟩

structure add_group_hom (α β : Type) [add_group α] [add_group β] :=
( to_fun : α → β )
( map_add : ∀ (a b), to_fun (a + b) = to_fun a + to_fun b )

instance add_group_hom.coe_to_fun (α β : Type) [add_group α] [add_group β] : 
  has_coe_to_fun' (add_group_hom α β) α β := ⟨add_group_hom.to_fun⟩

structure ring_hom (α β : Type) [ring α] [ring β] extends add_group_hom α β :=
( map_mul : ∀ (a b), to_fun (a * b) = to_fun a * to_fun b )
( map_one : to_fun 1 = 1 )

instance ring_hom.coe_to_fun (α β : Type*) [ring α] [ring β] : 
  has_coe_to_fun' (ring_hom α β) α β := ⟨ring_hom.to_fun⟩

class has_map_add (Γ α β : Type) [has_coe_to_fun' Γ α β] [add_group α]
  [add_group β] :=
( map_add : ∀ (f : Γ) (a b : α), f (a + b) = f a + f b ) 

instance add_group_hom.has_map_add (α β : Type) [add_group α] [add_group β] : 
  has_map_add (add_group_hom α β) α β :=
⟨add_group_hom.map_add⟩

instance ring_hom.has_map_add (α β : Type) [ring α] [ring β] : has_map_add (ring_hom α β) α β :=
⟨ring_hom.map_add⟩

attribute [simp] has_map_add.map_add

example (f : ring_hom ℤ ℤ) (a b : ℤ) : f a + f b = f (a + b) :=
begin
  simp,

end