Zulip Chat Archive

Stream: new members

Topic: how to convert a rational polynomial into a polynomial oR[x]


Jujian Zhang (Dec 05 2019 at 17:56):

I am experiementing with algebraic number, and this is what the goal became

import ring_theory.algebra data.real.basic

example : (2 : )⁻¹ + (-1) / algebra_map  (2 : ) = 0 := sorry

How should I get rid of the algebra_map

Patrick Massot (Dec 05 2019 at 18:18):

show (2 : ℝ)⁻¹ + (-1) / (2 : ℚ) = 0, by norm_num


Last updated: Dec 20 2023 at 11:08 UTC