α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ g (f x + f y) = g (f x) + g (f y)
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ (g ∘ f) (x + y) = (g ∘ f) x + (g ∘ f) y
simp [map_add hf]
no goals
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ g (f x + f y) = g (f x) + g (f y)
rw [map_add hg]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ g (f x * f y) = g (f x) * g (f y)
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
simp [map_mul hf]
no goals
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ g (f x * f y) = g (f x) * g (f y)
rw [map_mul hg]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
⊢ g 1 = 1
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
⊢ (g ∘ f) 1 = 1
simp [map_one hf]
no goals
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
⊢ g 1 = 1
exact map_one hg