## 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: May 14 2021 at 23:14 UTC