no goals
M₀ : Type u_1
G₀ : Type ?u.1682
M₀' : Type u_2
G₀' : Type ?u.1688
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
inst✝ : NoZeroDivisors M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
a✝ b✝ : M₀
H : a✝ * b✝ = 0
⊢ f (?m.2148 f hf zero mul H) * f (?m.2149 f hf zero mul H) = 0
rw [← mul, H, zero]
no goals
M₀ : Type u_1
G₀ : Type ?u.1682
M₀' : Type u_2
G₀' : Type ?u.1688
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
inst✝ : NoZeroDivisors M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
a✝ b✝ : M₀
H✝ : a✝ * b✝ = 0
this : f a✝ * f b✝ = 0
H : f a✝ = 0
⊢ f a✝ = f 0
rwa [zero]
no goals
M₀ : Type u_1
G₀ : Type ?u.1682
M₀' : Type u_2
G₀' : Type ?u.1688
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
inst✝ : NoZeroDivisors M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
a✝ b✝ : M₀
H✝ : a✝ * b✝ = 0
this : f a✝ * f b✝ = 0
H : f b✝ = 0
⊢ f b✝ = f 0
rwa [zero]