Zulip Chat Archive
Stream: new members
Topic: how to convert a real polynomial to a complex polynomial
Jiatong Yang (Feb 05 2025 at 01:42):
How to convert a real polynoimal to a complex polynomial in Lean4?
Aaron Liu (Feb 05 2025 at 01:56):
If you have a p : Polynomial Real, then p.map Complex.ofRealHom : Polynomial Complex
Eric Wieser (Feb 05 2025 at 04:56):
You might also be content to use docs#Polynomial.aroots
Last updated: May 02 2025 at 03:31 UTC