finsupp — Mathlib

English

If M has the IsSMulRegular with respect to k, then the finsupp space α →₀ M also has IsSMulRegular with respect to k. Regularity lifts from the coefficient module to the finsupp module.

Русский

Если M удовлетворяет условию IsSMulRegular для скаляра k, то и Finsupp α M удовлетворяет этому условию; регулярность поднимается от M к Finsupp α M.

LaTeX

$$$\\text{IsSMulRegular } M\\ k \\Rightarrow \\text{IsSMulRegular } (\\alpha \\to_0 M) \\ k$$$

Lean4

theorem _root_.IsSMulRegular.finsupp [Zero M] [SMulZeroClass R M] {k : R} (hk : IsSMulRegular M k) :
    IsSMulRegular (α →₀ M) k := fun _ _ h => ext fun i => hk (DFunLike.congr_fun h i)

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