mul_mem_nonZeroDivisors — Mathlib

English

For any a,b in M0, ab is a nonzero-divisor if and only if both a and b are nonzero-divisors.

Русский

Для любых a,b в M0, ab является ненулевым делителем тогда и только тогда, когда и a, и b — ненулевые делители.

LaTeX

$$mul_mem_nonZeroDivisors : a * b ∈ M0⁰ ↔ a ∈ M0⁰ ∧ b ∈ M0⁰$$

Lean4

theorem mul_mem_nonZeroDivisors : a * b ∈ M₀⁰ ↔ a ∈ M₀⁰ ∧ b ∈ M₀⁰
    where
  mp
    h := by
    rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
    constructor <;> intro x h' <;> apply h.2
    · rw [← mul_assoc, h', zero_mul]
    · rw [mul_comm a b, ← mul_assoc, h', zero_mul]
  mpr := fun h ↦ mul_mem h.1 h.2

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