Grace/Cumulus/Complex/Numeral.g17

Imports

Declarations

complexNumeral.pair theorem derivation
complexNumeral.member theorem derivation
complexNumeral.nonzero theorem derivation
Source

1-- Numerals of ℂ: the numeral n in a complex ring scope is the pair (n, 0),2-- so 3 may be written in place of 1 + 1 + 1.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Complex.Numeral9import Ring10import Real.Natural11import Real.RootTwo1213section Numerals14notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)15notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1617theorem complexNumeral.pair (n : Nat)18  shows ringNat(complexAdd, complexZero, complexOne, n) =19    (realNumeral(n), realZero)20proof21  induction n22  | zero =>23    rw [ringNat.zero, realNumeral.nat, realNat.zero]24    unfold complexZero25    rfl26  | succ(k) using ih =>27    have step := realNumeral.succ at k with *28    have pair := complexAdd.pair at realNumeral(k), realZero, realOne,29      realZero with *30    have second : R[realZero + realZero] = realZero by linarith31    rw [ringNat.succ, ih, step]32    unfold complexOne33    simp [pair, second]3435theorem complexNumeral.member (n : Nat)36  shows ringNat(complexAdd, complexZero, complexOne, n) ∈ ℂ37proof38  have pair := complexNumeral.pair at n with *39  have real := realNumeral.real at n with *40  rw pair41  typecheck4243-- A nonzero numeral is a nonzero complex number.44theorem complexNumeral.nonzero (n : Nat)45  requires positive : 0 < n46  shows ringNat(complexAdd, complexZero, complexOne, n) ≠ ℂ[0]47proof48  intro same49  have pair := complexNumeral.pair at n with *50  rw pair at same51  unfold complexZero at same52  have coordinates := orderedPair.injective with same53  have first := coordinates.left54  have real := realNumeral.real at n with *55  have bridge := realNumeral.nat at n with *56  rw bridge at first57  have below := realNat.lt_of_lt at 0, n with *58  rw realNat.zero at below59  linarith6061end Numerals62