Integral elements of ℂ

This file proves that Complex.I is integral over ℤ and ℚ.

theorem Complex.isIntegral_int_I : IsIntegral ℤ Complex.I

theorem Complex.isIntegral_rat_I : IsIntegral ℚ Complex.I