instNoZeroSMulDivisorsLocalizationLocalizedModule

English

If M has NoZeroSmulDivisors as an R-module, then Localization S provides NoZeroSmulDivisors on LocalizedModule S M.

Русский

Если M имеет свойство NoZeroSmulDivisors как модуль над R, то локализация S обеспечивает это свойство на LocalizedModule S M.

LaTeX

$$$\text{NoZeroSMulDivisors}(R,M) \Rightarrow \text{NoZeroSMulDivisors}(\mathrm{Localization}\;S, \mathrm{LocalizedModule}\;S\;M)$$$

Lean4

instance (S : Submonoid R) [NoZeroSMulDivisors R M] : NoZeroSMulDivisors (Localization S) (LocalizedModule S M) :=
  noZeroSMulDivisors (LocalizedModule.mkLinearMap S M) S

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