instNoZeroDivisors — Mathlib

English

A monomial with any index is a left non-zero-divisor when its coefficient is so in R.

Русский

Мономиал с любым индексом является левым ненулевым делителем, если его коэффициент таков в R.

LaTeX

$$$\forall n,\ (\mathrm{monomial}(n))\, r \in \mathrm{nonZeroDivisorsLeft}(R) \Rightarrow \mathrm{monomial}(n)\, r \in \mathrm{nonZeroDivisorsLeft}(\mathrm{MvPowerSeries}(\sigma,R)).$$$

Lean4

instance : NoZeroDivisors (MvPowerSeries σ R) where
  eq_zero_or_eq_zero_of_mul_eq_zero {φ ψ}
    h := by
    letI : LinearOrder σ := LinearOrder.swap σ WellOrderingRel.isWellOrder.linearOrder
    letI : WellFoundedGT σ := by
      change IsWellFounded σ fun x y ↦ WellOrderingRel x y
      exact IsWellOrder.toIsWellFounded
    simpa only [← lexOrder_eq_top_iff_eq_zero, lexOrder_mul, WithTop.add_eq_top] using h

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