toNoZeroSMulDivisors — Mathlib

English

If R has no zero divisors, then the multiplication on R by itself has NoZeroSMulDivisors.

Русский

Если в кольце R нет нулевых делителей, то умножение на R само на R имеет свойство NoZeroSMulDivisors.

LaTeX

$$NoZeroSMulDivisors R R$$

Lean4

instance (priority := 100) toNoZeroSMulDivisors [Zero R] [Mul R] [NoZeroDivisors R] : NoZeroSMulDivisors R R :=
  ⟨fun {_ _} => eq_zero_or_eq_zero_of_mul_eq_zero⟩

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