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

Stream: new members

[Jujian Zhang]

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]

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