distribSMul' — Mathlib

English

The quotient M/P inherits a DistribSMul structure from M, i.e., a • (x + y) = a•x + a•y, since mk respects addition.

Русский

Через отображение mk фактор-модуля M/P наследуется распределение умножения на скаляры: a • (x + y) = a•x + a•y.

LaTeX

$$$\forall a \in S,\forall x,y \in M,\ a \cdot (\mathrm{mk}(x) + \mathrm{mk}(y)) = \mathrm{mk}(a \cdot x) + \mathrm{mk}(a \cdot y)$$$

Lean4

instance distribSMul' [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) : DistribSMul S (M ⧸ P) :=
  fast_instance%Function.Surjective.distribSMul { toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl }
      Quot.mk_surjective (Submodule.Quotient.mk_smul P)

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