case h
F : Type ?u.127699
α : Type u_1
β : Type u_2
γ : Type ?u.127708
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
⊢ ∀ (x : β), ↑↑(mkRingHomOfMulSelfOfTwoNeZero f h h_two h_one) x = ↑f x
F : Type ?u.127699
α : Type u_1
β : Type u_2
γ : Type ?u.127708
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
⊢ ↑(mkRingHomOfMulSelfOfTwoNeZero f h h_two h_one) = f
apply AddMonoidHom.ext
case h
F : Type ?u.127699
α : Type u_1
β : Type u_2
γ : Type ?u.127708
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x✝ : β
⊢ ↑↑(mkRingHomOfMulSelfOfTwoNeZero f h h_two h_one) x✝ = ↑f x✝
case h
F : Type ?u.127699
α : Type u_1
β : Type u_2
γ : Type ?u.127708
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
⊢ ∀ (x : β), ↑↑(mkRingHomOfMulSelfOfTwoNeZero f h h_two h_one) x = ↑f x
intro
no goals
case h
F : Type ?u.127699
α : Type u_1
β : Type u_2
γ : Type ?u.127708
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x✝ : β
⊢ ↑↑(mkRingHomOfMulSelfOfTwoNeZero f h h_two h_one) x✝ = ↑f x✝
rfl