F : Type ?u.112165
α : Type ?u.112168
β : Type ?u.112171
R : Type ?u.112174
S : Type ?u.112177
S' : Type ?u.112180
inst✝⁶ : Add R
inst✝⁵ : Add S
inst✝⁴ : Mul R
inst✝³ : Mul S
A : Type u_1
B : Type u_2
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : NoZeroDivisors B
e : A ≃+* B
x y : A
hxy : x * y = 0
this : ↑e x * ↑e y = 0
⊢ x = 0 ∨ y = 0
F : Type ?u.112165
α : Type ?u.112168
β : Type ?u.112171
R : Type ?u.112174
S : Type ?u.112177
S' : Type ?u.112180
inst✝⁶ : Add R
inst✝⁵ : Add S
inst✝⁴ : Mul R
inst✝³ : Mul S
A : Type u_1
B : Type u_2
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : NoZeroDivisors B
e : A ≃+* B
x y : A
hxy : x * y = 0
⊢ x = 0 ∨ y = 0
have : e x * e y = 0 := by rw [← e.map_mul, hxy, e.map_zero]
no goals
F : Type ?u.112165
α : Type ?u.112168
β : Type ?u.112171
R : Type ?u.112174
S : Type ?u.112177
S' : Type ?u.112180
inst✝⁶ : Add R
inst✝⁵ : Add S
inst✝⁴ : Mul R
inst✝³ : Mul S
A : Type u_1
B : Type u_2
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : NoZeroDivisors B
e : A ≃+* B
x y : A
hxy : x * y = 0
this : ↑e x * ↑e y = 0
⊢ x = 0 ∨ y = 0
simpa using eq_zero_or_eq_zero_of_mul_eq_zero this
no goals
F : Type ?u.112165
α : Type ?u.112168
β : Type ?u.112171
R : Type ?u.112174
S : Type ?u.112177
S' : Type ?u.112180
inst✝⁶ : Add R
inst✝⁵ : Add S
inst✝⁴ : Mul R
inst✝³ : Mul S
A : Type u_1
B : Type u_2
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : NoZeroDivisors B
e : A ≃+* B
x y : A
hxy : x * y = 0
⊢ ↑e x * ↑e y = 0
rw [← e.map_mul, hxy, e.map_zero]