instNoZeroSMulDivisorsSubtypeMemSubmodule

English

Under appropriate scalar-tower assumptions, restricting scalars to R on a submodule I of S A preserves the NoZeroSmulDivisors property; i.e., I is NoZeroSmulDivisors over R.

Русский

При заданных условиях касающихся действий скалярных доменов, подмодуль I пары S A может сохранять свойство без нулевых делителей под действием скаляров R.

LaTeX

$$$ NoZeroSmulDivisors\\, R\\, I$$$

Lean4

instance {S A : Type*} [Semiring S] [SMul R S] [AddCommMonoid A] [Module R A] [Module S A] [IsScalarTower R S A]
    [NoZeroSMulDivisors R A] {I : Submodule S A} : NoZeroSMulDivisors R I :=
  Submodule.noZeroSMulDivisors (Submodule.restrictScalars R I)

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