noZeroSMulDivisors — Mathlib

English

If M has NoZeroSmulDivisors as an R-module, then the finsupp space ι →₀ M also has NoZeroSmulDivisors with respect to R.

Русский

Если у M есть свойство NoZeroSmulDivisors как R-модуля, то и ι →₀ M обладает NoZeroSmulDivisors относительно R.

LaTeX

$$$[Zero R][Zero M][SMulZeroClass R M][NoZeroSmulDivisors R M] \\Rightarrow NoZeroSmulDivisors R (\\iota \\to_0 M)$$$

Lean4

instance noZeroSMulDivisors [Zero R] [Zero M] [SMulZeroClass R M] {ι : Type*} [NoZeroSMulDivisors R M] :
    NoZeroSMulDivisors R (ι →₀ M) :=
  ⟨fun h =>
    or_iff_not_imp_left.mpr fun hc =>
      Finsupp.ext fun i => (eq_zero_or_eq_zero_of_smul_eq_zero (DFunLike.ext_iff.mp h i)).resolve_left hc⟩

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