leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

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

Theme Simple by wildflame © 2016 Powered by jekyll