instNoZeroDivisors — Mathlib

English

If Γ is ordered and additive cancellative, and R is a ring with no zero divisors, then HahnSeries Γ R has no zero divisors.

Русский

Если Γ упорядочено и остаётся свойство отсутствия нулевых делителей, то HahnSeries Γ R не имеет нулевых делителей.

LaTeX

$$$[IsDomain R] \\Rightarrow NoZeroDivisors(\\mathrm{HahnSeries}(\\Gamma,R))$$$

Lean4

instance {Γ} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R]
    [NoZeroDivisors R] : NoZeroDivisors (HahnSeries Γ R) where
  eq_zero_or_eq_zero_of_mul_eq_zero {x y}
    xy := by
    haveI : NoZeroSMulDivisors (HahnSeries Γ R) (HahnSeries Γ R) := HahnModule.instNoZeroSMulDivisors
    exact eq_zero_or_eq_zero_of_smul_eq_zero xy

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