product of functions in coerced codomain

Stream: Is there code for X?

[Yoh Tanimoto]

Hello!
Is there a simple way to write a product of f1 : X → ℂ f2 : X → ℝ? Writing f1 * f2 gives an error. Of course one can write def f3 : X → ℂ := fun x => f1 x * f2 x, but is there a reason why there is no coercion from X → ℝ to X → ℂ when there is a coercion ℝ → ℂ?

import Mathlib

variable (f1 : X → ℂ) (f2 : X → ℝ)
#check f1 * f2 -- failed to synthesize instance  HMul (X → ℂ) (X → ℝ) ?m.19669
def f3 := fun x => f1 x * f2 x
#check f3 f1 f2

[Edward van de Meent]

f2 • f1 should do the trick. important to note is that in this case, the function to ℝ has to be on the left side for this notation

[Edward van de Meent]

also, it works for any f2:X → Y as long as there is an instance SMul Y ℝ (or more generally SMul Y ℂ)

[Yaël Dillies]

The reason why there is no coercion from X → ℝ to X → ℂ is that it would lead to pretty poor performance

[Michael Stoll]

#check f1 * ((f2 ·) : X → ℂ) also works.

[Eric Wieser]

Edward van de Meent said:

f2 • f1 should do the trick.

Note this approach can behave unpredictably if the right function takes two arguments (for instance, is a vector-valued function where the second argument is the index) but the left takes one.

[Yoh Tanimoto]

ok, thanks to you all for your replies!
so is there a common/canonical choice or one just uses a preferred way?

actually I wanted to take f1 : C₀(X, ℂ) f2 : C₀(X, ℝ) and have that f1 * f2 : C₀(X, ℂ). there are several ways to do an equivalent thing, and I wonder which is the best.