Gaussian_Rationals_form_Subfield_of_Complex_Numbers
Provedalgebracomplex-numbersproofwiki
The set of Gaussian rationals Q[i] forms a subfield of the complex numbers.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Gaussian_Rationals_form_Subfield_of_Complex_Numbers : ∀ a b : ℚ, ((↑a + ↑b * Complex.I : ℂ) + (↑a + ↑b * Complex.I : ℂ)) = (↑(a + a) + ↑(b + b) * Complex.I : ℂ) := by sorry
Source