[isabelle] fsp question-- supporting "natural" entry
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
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
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".
From the QED manifesto: https://www.cs.ru.nl/~freek/qed/qed.html
Mathematics is arguably the foremost creation of the human mind.
This archive was generated by a fusion of
Pipermail (Mailman edition) and