noZeroDivisors_iff — Mathlib

English

NoZeroDivisors for the polynomial ring R[X] is equivalent to NoZeroDivisors for the base ring R.

Русский

Свойство отсутствия нулевых делителей в кольце многочленов R[X] эквивалентно отсутствию нулевых делителей в базовом кольце R.

LaTeX

$$NoZeroDivisors(R[X]) \leftrightarrow NoZeroDivisors(R)$$

Lean4

/-- See also `Polynomial.isCancelMulZero_iff`: in order for `R[X]` to have cancellative
multiplication (stronger than `NoZeroDivisors` in general, but equivalent if `R` is a ring),
`R` must have both cancellative multiplication and cancellative addition. -/
theorem noZeroDivisors_iff : NoZeroDivisors R[X] ↔ NoZeroDivisors R
    where
  mp _ := C_injective.noZeroDivisors _ C_0 fun _ _ ↦ C_mul
  mpr _ := inferInstance

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