ComplexField

The concrete complex field and its elementary arithmetic

Open in Workbench View on GitHub

1-- The concrete complex field and its elementary arithmetic.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module ComplexField8import Grace.Cumulus.Complex910section Complexes11notation ring C := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)12notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1314theorem field15  shows IsField(C)16proof17  exact complexes.is_field1819theorem square_of_i20  shows C[(R[0], R[1]) * (R[0], R[1])] = C[-1]21proof22  have zero := realZero.real23  have one := realOne.real24  have realPart : R[0 * 0 - 1 * 1] = R[-1] by ring25  have imaginaryPart : R[0 * 1 + 1 * 0] = R[0] by ring26  have negZero : R[-0] = R[0] by ring27  simp [complexOne, complexMul.pair, complexNeg.pair]2829theorem inverse (a b : Real)30  requires nonzero : (a, b) ≠ C[0]31  shows IsInverse(complexCarrier, complexMul, complexOne, (a, b),32    (R[a * realInvValue(a * a + b * b)], R[-b * realInvValue(a * a + b * b)]))33proof34  exact complex.inverse_pair with *3536end Complexes37