instNoZeroSMulDivisors — Mathlib

English

If S-NoZeroSmulDivisors holds for N, then the space of alternating multilinear maps from M to N also has no zero-smul divisors under the induced S-action.

Русский

Если на модуле N над S выполняется свойство нет нулевых делителей умножения, то и пространство чередующихся многолинейных отображений из M в N, снабжённое индуцированным действием S, обладает этим свойством.

LaTeX

$$$ \mathrm{NoZeroSmulDivisors}_S \left( M [\⋀^ι] \to_{\_R} N \right)$$$

Lean4

instance instNoZeroSMulDivisors [NoZeroSMulDivisors S N] : NoZeroSMulDivisors S (M [⋀^ι]→ₗ[R] N) :=
  coe_injective.noZeroSMulDivisors _ rfl coeFn_smul

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