Dezimalzahlen multiplizieren

Gibt es einen Weg, mit dem man Dezimalzahlen multiplizieren kann?
Die Funktion $mul nimmt anscheinend bei einer Zahl mit Dezimalzahl nur den ganzzahligen Rest, z.B.
$mul(1,5 ,20) gibt 20 und nicht 30.
auch
$mul(1.5 ,20) gibt 20.

Gibt es so eine $val-Funktion oder so?

Das Komma weglassen und am Ende dividieren:
$div($mul($replace('1,5',',',),20),10)
$div($mul($replace('1,5',$char(44),),20),10)

Ach ja! Danke.
Ich habe mir die Freiheit genommen, die neu gewonnen Kenntnisse in diesem Thread weiterzugeben:
Replace Tags from other Tags