F : Type ?u.113908
α : Type ?u.113911
β : Type ?u.113914
R : Type ?u.113917
S : Type ?u.113920
S' : Type ?u.113923
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✝ : IsDomain B
e : A ≃+* B
this : Nontrivial A
⊢ IsDomain A
F : Type ?u.113908
α : Type ?u.113911
β : Type ?u.113914
R : Type ?u.113917
S : Type ?u.113920
S' : Type ?u.113923
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✝ : IsDomain B
e : A ≃+* B
⊢ IsDomain A
haveI : Nontrivial A := ⟨⟨e.symm 0, e.symm 1, e.symm.injective.ne zero_ne_one⟩⟩
F : Type ?u.113908
α : Type ?u.113911
β : Type ?u.113914
R : Type ?u.113917
S : Type ?u.113920
S' : Type ?u.113923
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✝ : IsDomain B
e : A ≃+* B
this✝ : Nontrivial A
this : NoZeroDivisors A
⊢ IsDomain A
F : Type ?u.113908
α : Type ?u.113911
β : Type ?u.113914
R : Type ?u.113917
S : Type ?u.113920
S' : Type ?u.113923
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✝ : IsDomain B
e : A ≃+* B
this : Nontrivial A
⊢ IsDomain A
haveI := e.noZeroDivisors B
no goals
F : Type ?u.113908
α : Type ?u.113911
β : Type ?u.113914
R : Type ?u.113917
S : Type ?u.113920
S' : Type ?u.113923
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✝ : IsDomain B
e : A ≃+* B
this✝ : Nontrivial A
this : NoZeroDivisors A
⊢ IsDomain A
exact NoZeroDivisors.to_isDomain _