have : ((0 : ℤα) : ℂ) = 0 := my_map_zero
a b c : ℤα
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0