Theorems · Theorem · ring theory

MulEquiv.isDomain

∀ {A : Type u_7} (B : Type u_8) [inst : Semiring A] [inst_1 : Semiring B] [IsDomain B] (e : A ≃* B), IsDomain A

If two rings are isomorphic, and the second is a domain, then so is the first.

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

8 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

SemiringSemiringIsDomain