noZeroDivisors — Mathlib

English

If A ≃* B and B has no zero divisors, then A also has no zero divisors.

Русский

Если существует изоморфизм колец A ≃* B и B не имеет нулевых делителей, то и A не имеет нулевых делителей.

LaTeX

$$$ \text{NoZeroDivisors}(A) \Rightarrow \text{NoZeroDivisors}(B) \text{ under an isomorphism}$$$

Lean4

/-- If two rings are isomorphic, and the second doesn't have zero divisors,
then so does the first. -/
protected theorem noZeroDivisors {A : Type*} (B : Type*) [MulZeroClass A] [MulZeroClass B] [NoZeroDivisors B]
    (e : A ≃* B) : NoZeroDivisors A :=
  e.injective.noZeroDivisors e (map_zero e) (map_mul e)

Похожие утверждения