English
If A ≃* B and B is a domain, then A is a domain; and conversely, if A is a domain, then B is a domain.
Русский
Если A ≃* B и B является доменом, то A также является доменом; и наоборот.
LaTeX
$$$ \text{IsDomain}(A) \iff \text{IsDomain}(B) \text{ under } e : A \simeq* B$$$
Lean4
/-- If two rings are isomorphic, and the second is a domain, then so is the first. -/
protected theorem isDomain {A : Type*} (B : Type*) [Semiring A] [Semiring B] [IsDomain B] (e : A ≃* B) : IsDomain A :=
{ e.injective.isLeftCancelMulZero e (map_zero e) (map_mul e),
e.injective.isRightCancelMulZero e (map_zero e) (map_mul e) with
exists_pair_ne := ⟨e.symm 0, e.symm 1, e.symm.injective.ne zero_ne_one⟩ }
