instDistribMulAction — Mathlib

English

There is a natural action of the ring (or semiring) R on the space of continuous alternating maps M [⋀^ι]→L[A] N given pointwise: (r · f)(m) = r · f(m). This action distributes over addition and respects scalar multiplication.

Русский

Существует естественное действие кольца R на пространство непрерывных чередующих отображений M [⋀^ι]→L[A] N: (r · f)(m) = r · f(m). Это действие распределимо по сложению и согласуется с умножением на скаляры.

LaTeX

$$$$ (r) \\cdot (f + g) = r\\cdot f + r\\cdot g, \\quad (rs)\\cdot f = r\\cdot (s\\cdot f) $$ для любых f,g и r,s, где (r·f)(m) = r·f(m). $$$$

Lean4

instance [ContinuousAdd N] : DistribMulAction R (M [⋀^ι]→L[A] N) :=
  Function.Injective.distribMulAction toMultilinearAddHom toContinuousMultilinearMap_injective fun _ _ => rfl

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