case eq_zero
R S : Type u
x y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
⊢ ∀ (x : R), IsNilpotent x → x = 0
R S : Type u
x y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
⊢ IsReduced R
constructor
case eq_zero
R S : Type u
x✝ y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ x = 0
case eq_zero
R S : Type u
x y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
⊢ ∀ (x : R), IsNilpotent x → x = 0
intro x hx
case eq_zero.a
R S : Type u
x✝ y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ ↑f x = ↑f 0
case eq_zero
R S : Type u
x✝ y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ x = 0
apply hf
case eq_zero.a
R S : Type u
x✝ y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ ↑f x = 0
case eq_zero.a
R S : Type u
x✝ y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ ↑f x = ↑f 0
rw [map_zero]
no goals
case eq_zero.a
R S : Type u
x✝ y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ ↑f x = 0
exact (hx.map f).eq_zero