English
If Γ is an ordered additive monoid and R is a ring with a no-zero-smul-divisors property relative to a Hahn module, then the pair HahnSeries Γ R and HahnModule Γ R V has NoZeroSmulDivisors.
Русский
Если Γ — упорядоченный аддитивный моноид, R — кольцо и выполняется свойство Нет нулевых делителей умножения, то HahnSeries Γ R и HahnModule Γ R V образуют пару без нулевых делителей умножения.
LaTeX
$$$\\text{NoZeroSmulDivisors}(\\mathrm{HahnSeries}(\\Gamma,R), \\mathrm{HahnModule}(\\Gamma,R,V))$$$
Lean4
instance instNoZeroSMulDivisors {Γ} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Zero R]
[SMulWithZero R V] [NoZeroSMulDivisors R V] : NoZeroSMulDivisors (HahnSeries Γ R) (HahnModule Γ R V) where
eq_zero_or_eq_zero_of_smul_eq_zero {x y}
hxy := by
contrapose! hxy
simp only [ne_eq]
rw [HahnModule.ext_iff, funext_iff, not_forall]
refine ⟨x.order + ((of R).symm y).order, ?_⟩
rw [coeff_smul_order_add_order x y, of_symm_zero, HahnSeries.coeff_zero, smul_eq_zero, not_or]
constructor
· exact HahnSeries.leadingCoeff_ne_zero.mpr hxy.1
· exact HahnSeries.leadingCoeff_ne_zero.mpr hxy.2
