instDistribMulActionShrink — Mathlib

English

If M is a monoid and α is an AddCommMonoid with a distributive action of M, then Shrink α inherits a distributive action of M via the natural equivalence Shrink α ≃ α.

Русский

Если M — моноид, α — коммутативный аддитивный моноид и на α задано распределённое действие M, то Shrink α наследует распределённое действие M через естественную эквиваленцию Shrink α ≃ α.

LaTeX

$$$\\\\operatorname{DistribMulAction} \\\\ M \\\\ (\\\\operatorname{Shrink}(\\\\alpha))$$$

Lean4

instance [Monoid M] [AddCommMonoid α] [DistribMulAction M α] : DistribMulAction M (Shrink.{v} α) :=
  (equivShrink α).symm.distribMulAction M

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