instNoZeroDivisorsFinsuppNat — Mathlib

English

If R has no zero divisors and σ is finite, then the Hahn series HahnSeries (Finsupp σ Nat) R has no zero divisors.

Русский

Если в кольце R нет нулевых делителей и σ конечно, то HahnSeries (Finsupp σ Nat) R не имеет нулевых делителей.

LaTeX

$$$\\text{NoZeroDivisors}(R) \\Rightarrow \\big(\\text{Finite}(σ) \\Rightarrow \\text{NoZeroDivisors}(HahnSeries(Finsupp\\,σ\\,Nat)\\,R)\\big)$$$

Lean4

/-- If R has no zero divisors and `σ` is finite,
then `HahnSeries (σ →₀ ℕ) R` has no zero divisors -/
instance [NoZeroDivisors R] : NoZeroDivisors (HahnSeries (σ →₀ ℕ) R) :=
  toMvPowerSeries.toMulEquiv.noZeroDivisors (A := HahnSeries (σ →₀ ℕ) R) (MvPowerSeries σ R)

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