Email Gateway (Aug 22 2022 at 15:16): Email Gateway (Aug 22 2022 at 15:16):From: Raymond Rogers <raymond.rogers72@gmail.com>
Formal_Power_Series
has
lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d =
fps_const (c * d)"
for scalar multiplication of c times fsp and it works but seems to
require a conversion in the "shows" before entry. I would like to state
shows "(x::real)*(f::fsp)....."
or tacitly
shows "(x)*(f::fsp)....."
explicitly, but the parser objects.
In order to avoid continually digging around in the terms far removed in
the heirarchy, is it appropriate to "overload" "*" ? Can I even do it
to "*"? The documentation I am reading seems oriented to overloading
classes/types.
And should I do it or not. i.e. are there dangers here?
In addition: since the fsp can have coefficients from rings other than
real; how should I make sure that "x in (coefficient ring)" ?
I am really open to alternatives to "overloading"; but I would really
like equations far removed from the base to be expressible "naturally".
Ray
Last updated: Nov 21 2024 at 12:39 UTC