instNoZeroDivisorsOfUniqueProds — Mathlib

English

If R has no zero divisors and A has Mul and UniqueProds, then the MonoidAlgebra R A has no zero divisors.

Русский

Если R не имеет нулевых делителей, а A имеет свойство UniqueProds, то MonoidAlgebra R A также не имеет нулевых делителей.

LaTeX

$$$$\text{NoZeroDivisors }(MonoidAlgebra\ R\ A).$$$$

Lean4

instance [NoZeroDivisors R] [Mul A] [UniqueProds A] : NoZeroDivisors (MonoidAlgebra R A) where
  eq_zero_or_eq_zero_of_mul_eq_zero {a b}
    ab := by
    contrapose! ab
    obtain ⟨da, a0, db, b0, h⟩ :=
      UniqueProds.uniqueMul_of_nonempty (support_nonempty_iff.mpr ab.1) (support_nonempty_iff.mpr ab.2)
    refine support_nonempty_iff.mp ⟨da * db, ?_⟩
    rw [mem_support_iff] at a0 b0 ⊢
    exact mul_apply_mul_eq_mul_of_uniqueMul h ▸ mul_ne_zero a0 b0

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