noZeroDivisors_iff — Mathlib

English

NoZeroDivisors is preserved and reflected by ring isomorphisms: NoZeroDivisors A ↔ NoZeroDivisors B under e: A ≃* B.

Русский

NoZeroDivisors сохраняется и отражается при изоморфизмах колец: NoZeroDivisors A ↔ NoZeroDivisors B при e: A ≃* B.

LaTeX

$$$ \text{NoZeroDivisors}(A) \iff \text{NoZeroDivisors}(B) $$$

Lean4

theorem noZeroDivisors_iff (e : A ≃* B) : NoZeroDivisors A ↔ NoZeroDivisors B
    where
  mp _ := e.symm.noZeroDivisors
  mpr _ := e.noZeroDivisors

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