Documentation

FormalConjectures.Mathoverflow.«21003»

Mathoverflow 21003 #

Is there any polynomial $f(x, y) \in \mathbb{Q}[x, y]$ such that $f : \mathbb{Q} \times \mathbb{Q} \rightarrow \mathbb{Q}$ is a bijection?

Reference: mathoverflow/21003 asked by user Z.H.

theorem mathoverflow_21003 :
(∃ (f : MvPolynomial (Fin 2) ), Function.Bijective fun (x : Fin 2) => (MvPolynomial.eval x) f) sorry

Is there any polynomial $f(x, y) \in \mathbb{Q}[x, y]$ such that $f : \mathbb{Q} \times \mathbb{Q} \rightarrow \mathbb{Q}$ is a bijection?