instDistribSMul — Mathlib

English

Let A be an additive zero class with a scalar action by M that is distributive and continuous; then the SeparationQuotient A inherits a distributive scalar action by M.

Русский

Пусть A — аддитивная ноль-класс с действием скалярами M, удовлетворяющим свойству распределимости и непрерывности; тогда SeparationQuotient A наследует распределённое действие скаляров M.

LaTeX

$$$\mathrm{DistribSMul}\ M (\mathrm{SeparationQuotient} A)$$$

Lean4

instance instDistribSMul [AddZeroClass A] [DistribSMul M A] [ContinuousAdd A] [ContinuousConstSMul M A] :
    DistribSMul M (SeparationQuotient A) :=
  surjective_mk.distribSMul mkAddMonoidHom mk_smul

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