Multiplicative maps applied entrywise

A multiplicative map applied entrywise to a scalar multiple c • v of a family gives f c • (f ∘ v). This is the scalar companion of Mathlib's map_comp_mul and map_comp_pow.

Main results

• TauCeti.map_comp_smul: f ∘ (c • v) = f c • (f ∘ v).

@[simp]

theorem TauCeti.map_comp_smul {F : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (c : M) (v : ι → M) : ⇑f ∘ (c • v) = f c • ⇑f ∘ v

A multiplicative map applied entrywise to c • v gives f c • (f ∘ v).