English
Let l be a list of elements of N and m ∈ M with suitable actions. Then m^{|l|} • l.prod = ∏ x∈l, m • x.
Русский
Пусть l — список элементов N, и m действует; тогда m^{|l|} • (произведение элементов списка) = произведение элементoв списка после действия: ∏(m•x).
LaTeX
$$$\\forall {M} {N} [\\mathsf{Monoid} M] [\\mathsf{MulOneClass} N] [\\mathsf{MulAction} M N] [\\mathsf{IsScalarTower} M N N] [\\mathsf{SMulCommClass} M N N] (l:\\mathsf{List} N) (m:M),\\; m^{|l|} \\cdot l.prod = \\prod x\\in l, m \\cdot x$$$
Lean4
@[to_additive]
theorem smul_prod [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (l : List N)
(m : M) : m ^ l.length • l.prod = (l.map (m • ·)).prod := by
induction l with
| nil => simp
| cons head tail ih => simp [← ih, smul_mul_smul_comm, pow_succ']
