instNoZeroSMulDivisors — Mathlib

English

If S acts on M' with NoZeroSmulDivisors, then the space of σ-linear maps M → M' inherits NoZeroSmulDivisors as an S-module.

Русский

Если S действует на M' с NoZeroSmulDivisors, то пространство σ-линейных отображений M → M' наследует это свойство как S-модуль.

LaTeX

$$NoZeroSmulDivisors S (LinearMap σ M M')$$

Lean4

instance [NoZeroSMulDivisors S M'] : NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M') :=
  coe_injective.noZeroSMulDivisors _ rfl coe_smul

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