instNoZeroDivisors — Mathlib

English

If R has no zero divisors, then the power series ring R[[X]] also has no zero divisors.

Русский

Если R не имеет нулевых делителей, то и кольцо степенных рядов R[[X]] не имеет нулевых делителей.

LaTeX

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

Lean4

instance [NoZeroDivisors R] : NoZeroDivisors R⟦X⟧ where
  eq_zero_or_eq_zero_of_mul_eq_zero {φ ψ}
    h := by
    simp_rw [← order_eq_top, order_mul] at h ⊢
    exact WithTop.add_eq_top.mp h

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