F : Type ?u.111124
α : Type u_1
β : Type u_2
γ : Type ?u.111133
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this : Nontrivial β
⊢ IsDomain β
F : Type ?u.111124
α : Type u_1
β : Type u_2
γ : Type ?u.111133
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
⊢ IsDomain β
haveI := pullback_nonzero f f.map_zero f.map_one
F : Type ?u.111124
α : Type u_1
β : Type u_2
γ : Type ?u.111133
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this✝ : Nontrivial β
this : NoZeroDivisors α
⊢ IsDomain β
F : Type ?u.111124
α : Type u_1
β : Type u_2
γ : Type ?u.111133
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this : Nontrivial β
⊢ IsDomain β
haveI := IsRightCancelMulZero.to_noZeroDivisors α
F : Type ?u.111124
α : Type u_1
β : Type u_2
γ : Type ?u.111133
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this✝¹ : Nontrivial β
this✝ : NoZeroDivisors α
this : NoZeroDivisors β
⊢ IsDomain β
F : Type ?u.111124
α : Type u_1
β : Type u_2
γ : Type ?u.111133
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this✝ : Nontrivial β
this : NoZeroDivisors α
⊢ IsDomain β
haveI := hf.noZeroDivisors f f.map_zero f.map_mul
no goals
F : Type ?u.111124
α : Type u_1
β : Type u_2
γ : Type ?u.111133
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this✝¹ : Nontrivial β
this✝ : NoZeroDivisors α
this : NoZeroDivisors β
⊢ IsDomain β
exact NoZeroDivisors.to_isDomain β