instDistribMulAction — Mathlib

English

If M acts on A by a distributive multiplicative action and A is an additive module with continuous action, then SeparationQuotient A inherits a distributive multiplicative action by M.

Русский

Если M действует на A через распределимое умножение и A имеет непрерывное действие, то SeparationQuotient A наследует распределимое действие умножения M.

LaTeX

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

Lean4

instance instDistribMulAction [Monoid M] [AddMonoid A] [DistribMulAction M A] [ContinuousAdd A]
    [ContinuousConstSMul M A] : DistribMulAction M (SeparationQuotient A) :=
  surjective_mk.distribMulAction mkAddMonoidHom mk_smul

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