- COMPLEX_LEMMA1
-
|- ∀a b c d.
(a * c − b * d) pow 2 + (a * d + b * c) pow 2 =
(a pow 2 + b pow 2) * (c pow 2 + d pow 2)
- COMPLEX_LEMMA2
-
|- ∀x y. abs x ≤ sqrt (x pow 2 + y pow 2)
- COMPLEX
-
|- ∀z. (RE z,IM z) = z
- COMPLEX_RE_IM_EQ
-
|- ∀z w. (z = w) ⇔ (RE z = RE w) ∧ (IM z = IM w)
- RE_COMPLEX_OF_REAL
-
|- ∀x. RE (complex_of_real x) = x
- IM_COMPLEX_OF_REAL
-
|- ∀x. IM (complex_of_real x) = 0
- COMPLEX_0
-
|- 0 = complex_of_real 0
- COMPLEX_1
-
|- 1 = complex_of_real 1
- COMPLEX_10
-
|- 1 ≠ 0
- COMPLEX_0_THM
-
|- ∀z. (z = 0) ⇔ (RE z pow 2 + IM z pow 2 = 0)
- COMPLEX_ADD_COMM
-
|- ∀z w. z + w = w + z
- COMPLEX_ADD_ASSOC
-
|- ∀z w v. z + (w + v) = z + w + v
- COMPLEX_ADD_RID
-
|- ∀z. z + 0 = z
- COMPLEX_ADD_LID
-
|- ∀z. 0 + z = z
- COMPLEX_ADD_RINV
-
|- ∀z. z + -z = 0
- COMPLEX_ADD_LINV
-
|- ∀z. -z + z = 0
- COMPLEX_MUL_COMM
-
|- ∀z w. z * w = w * z
- COMPLEX_MUL_ASSOC
-
|- ∀z w v. z * (w * v) = z * w * v
- COMPLEX_MUL_RID
-
|- ∀z. z * 1 = z
- COMPLEX_MUL_LID
-
|- ∀z. 1 * z = z
- COMPLEX_MUL_RINV
-
|- ∀z. z ≠ 0 ⇒ (z * inv z = 1)
- COMPLEX_MUL_LINV
-
|- ∀z. z ≠ 0 ⇒ (inv z * z = 1)
- COMPLEX_ADD_LDISTRIB
-
|- ∀z w v. z * (w + v) = z * w + z * v
- COMPLEX_ADD_RDISTRIB
-
|- ∀z w v. (z + w) * v = z * v + w * v
- COMPLEX_EQ_LADD
-
|- ∀z w v. (z + w = z + v) ⇔ (w = v)
- COMPLEX_EQ_RADD
-
|- ∀z w v. (z + v = w + v) ⇔ (z = w)
- COMPLEX_ADD_RID_UNIQ
-
|- ∀z w. (z + w = z) ⇔ (w = 0)
- COMPLEX_ADD_LID_UNIQ
-
|- ∀z w. (z + w = w) ⇔ (z = 0)
- COMPLEX_NEGNEG
-
|- ∀z. - -z = z
- COMPLEX_NEG_EQ
-
|- ∀z w. (-z = w) ⇔ (z = -w)
- COMPLEX_EQ_NEG
-
|- ∀z w. (-z = -w) ⇔ (z = w)
- COMPLEX_RNEG_UNIQ
-
|- ∀z w. (z + w = 0) ⇔ (w = -z)
- COMPLEX_LNEG_UNIQ
-
|- ∀z w. (z + w = 0) ⇔ (z = -w)
- COMPLEX_NEG_ADD
-
|- ∀z w. -(z + w) = -z + -w
- COMPLEX_MUL_RZERO
-
|- ∀z. z * 0 = 0
- COMPLEX_MUL_LZERO
-
|- ∀z. 0 * z = 0
- COMPLEX_NEG_LMUL
-
|- ∀z w. -(z * w) = -z * w
- COMPLEX_NEG_RMUL
-
|- ∀z w. -(z * w) = z * -w
- COMPLEX_NEG_MUL2
-
|- ∀z w. -z * -w = z * w
- COMPLEX_ENTIRE
-
|- ∀z w. (z * w = 0) ⇔ (z = 0) ∨ (w = 0)
- COMPLEX_NEG_0
-
|- -0 = 0
- COMPLEX_NEG_EQ0
-
|- ∀z. (-z = 0) ⇔ (z = 0)
- COMPLEX_SUB_REFL
-
|- ∀z. z − z = 0
- COMPLEX_SUB_RZERO
-
|- ∀z. z − 0 = z
- COMPLEX_SUB_LZERO
-
|- ∀z. 0 − z = -z
- COMPLEX_SUB_LNEG
-
|- ∀z w. -z − w = -(z + w)
- COMPLEX_SUB_NEG2
-
|- ∀z w. -z − -w = w − z
- COMPLEX_NEG_SUB
-
|- ∀z w. -(z − w) = w − z
- COMPLEX_SUB_RNEG
-
|- ∀z w. z − -w = z + w
- COMPLEX_SUB_ADD
-
|- ∀z w. z − w + w = z
- COMPLEX_SUB_ADD2
-
|- ∀z w. w + (z − w) = z
- COMPLEX_ADD_SUB
-
|- ∀z w. z + w − z = w
- COMPLEX_SUB_SUB
-
|- ∀z w. z − w − z = -w
- COMPLEX_SUB_SUB2
-
|- ∀z w. z − (z − w) = w
- COMPLEX_ADD_SUB2
-
|- ∀z w. z − (z + w) = -w
- COMPLEX_ADD2_SUB2
-
|- ∀z w u v. z + w − (u + v) = z − u + (w − v)
- COMPLEX_SUB_TRIANGLE
-
|- ∀z w v. z − w + (w − v) = z − v
- COMPLEX_SUB_0
-
|- ∀z w. (z − w = 0) ⇔ (z = w)
- COMPLEX_EQ_SUB_LADD
-
|- ∀z w v. (z = w − v) ⇔ (z + v = w)
- COMPLEX_EQ_SUB_RADD
-
|- ∀z w v. (z − w = v) ⇔ (z = v + w)
- COMPLEX_MUL_RNEG
-
|- ∀z w. z * -w = -(z * w)
- COMPLEX_MUL_LNEG
-
|- ∀z w. -z * w = -(z * w)
- COMPLEX_SUB_LDISTRIB
-
|- ∀z w v. z * (w − v) = z * w − z * v
- COMPLEX_SUB_RDISTRIB
-
|- ∀z w v. (z − w) * v = z * v − w * v
- COMPLEX_DIFFSQ
-
|- ∀z w. (z + w) * (z − w) = z * z − w * w
- COMPLEX_EQ_LMUL
-
|- ∀z w v. (z * w = z * v) ⇔ (z = 0) ∨ (w = v)
- COMPLEX_EQ_RMUL
-
|- ∀z w v. (z * v = w * v) ⇔ (v = 0) ∨ (z = w)
- COMPLEX_EQ_LMUL2
-
|- ∀z w v. z ≠ 0 ⇒ ((w = v) ⇔ (z * w = z * v))
- COMPLEX_EQ_RMUL_IMP
-
|- ∀z w v. z ≠ 0 ∧ (w * z = v * z) ⇒ (w = v)
- COMPLEX_EQ_LMUL_IMP
-
|- ∀z w v. z ≠ 0 ∧ (z * w = z * v) ⇒ (w = v)
- COMPLEX_NEG_INV
-
|- ∀z. z ≠ 0 ⇒ (inv (-z) = -inv z)
- COMPLEX_INV_MUL
-
|- ∀z w. z ≠ 0 ∧ w ≠ 0 ⇒ (inv (z * w) = inv z * inv w)
- COMPLEX_INVINV
-
|- ∀z. z ≠ 0 ⇒ (inv (inv z) = z)
- COMPLEX_LINV_UNIQ
-
|- ∀z w. (z * w = 1) ⇒ (z = inv w)
- COMPLEX_RINV_UNIQ
-
|- ∀z w. (z * w = 1) ⇒ (w = inv z)
- COMPLEX_INV_0
-
|- inv 0 = 0
- COMPLEX_INV1
-
|- inv 1 = 1
- COMPLEX_INV_INV
-
|- ∀z. inv (inv z) = z
- COMPLEX_INV_NEG
-
|- ∀z. inv (-z) = -inv z
- COMPLEX_INV_EQ_0
-
|- ∀z. (inv z = 0) ⇔ (z = 0)
- COMPLEX_INV_NZ
-
|- ∀z. z ≠ 0 ⇒ inv z ≠ 0
- COMPLEX_INV_INJ
-
|- ∀z w. (inv z = inv w) ⇔ (z = w)
- COMPLEX_NEG_LDIV
-
|- ∀z w. -(z / w) = -z / w
- COMPLEX_NEG_RDIV
-
|- ∀z w. -(z / w) = z / -w
- COMPLEX_NEG_DIV2
-
|- ∀z w. -z / -w = z / w
- COMPLEX_INV_1OVER
-
|- ∀z. inv z = 1 / z
- COMPLEX_DIV1
-
|- ∀z. z / 1 = z
- COMPLEX_DIV_ADD
-
|- ∀z w v. z / v + w / v = (z + w) / v
- COMPLEX_DIV_SUB
-
|- ∀z w v. z / v − w / v = (z − w) / v
- COMPLEX_DIV_RMUL_CANCEL
-
|- ∀v z w. v ≠ 0 ⇒ (z * v / (w * v) = z / w)
- COMPLEX_DIV_LMUL_CANCEL
-
|- ∀v z w. v ≠ 0 ⇒ (v * z / (v * w) = z / w)
- COMPLEX_DIV_DENOM_CANCEL
-
|- ∀z w v. z ≠ 0 ⇒ (w / z / (v / z) = w / v)
- COMPLEX_DIV_INNER_CANCEL
-
|- ∀z w v. z ≠ 0 ⇒ (w / z * (z / v) = w / v)
- COMPLEX_DIV_OUTER_CANCEL
-
|- ∀z w v. z ≠ 0 ⇒ (z / w * (v / z) = v / w)
- COMPLEX_DIV_MUL2
-
|- ∀z w. z ≠ 0 ∧ w ≠ 0 ⇒ ∀v. v / w = z * v / (z * w)
- COMPLEX_ADD_RAT
-
|- ∀z w u v. w ≠ 0 ∧ v ≠ 0 ⇒ (z / w + u / v = (z * v + w * u) / (w * v))
- COMPLEX_SUB_RAT
-
|- ∀z w u v. w ≠ 0 ∧ v ≠ 0 ⇒ (z / w − u / v = (z * v − w * u) / (w * v))
- COMPLEX_DIV_LZERO
-
|- ∀z. 0 / z = 0
- COMPLEX_DIV_REFL
-
|- ∀z. z ≠ 0 ⇒ (z / z = 1)
- COMPLEX_SUB_INV2
-
|- ∀z w. z ≠ 0 ∧ w ≠ 0 ⇒ (inv z − inv w = (w − z) / (z * w))
- COMPLEX_EQ_RDIV_EQ
-
|- ∀z w v. v ≠ 0 ⇒ ((z = w / v) ⇔ (z * v = w))
- COMPLEX_EQ_LDIV_EQ
-
|- ∀z w v. v ≠ 0 ⇒ ((z / v = w) ⇔ (z = w * v))
- COMPLEX_OF_REAL_EQ
-
|- ∀x y. (complex_of_real x = complex_of_real y) ⇔ (x = y)
- COMPLEX_OF_REAL_ADD
-
|- ∀x y. complex_of_real x + complex_of_real y = complex_of_real (x + y)
- COMPLEX_OF_REAL_NEG
-
|- ∀x. -complex_of_real x = complex_of_real (-x)
- COMPLEX_OF_REAL_MUL
-
|- ∀x y. complex_of_real x * complex_of_real y = complex_of_real (x * y)
- COMPLEX_OF_REAL_INV
-
|- ∀x. inv (complex_of_real x) = complex_of_real (inv x)
- COMPLEX_OF_REAL_SUB
-
|- ∀x y. complex_of_real x − complex_of_real y = complex_of_real (x − y)
- COMPLEX_OF_REAL_DIV
-
|- ∀x y. complex_of_real x / complex_of_real y = complex_of_real (x / y)
- COMPLEX_OF_NUM_EQ
-
|- ∀m n. (&m = &n) ⇔ (m = n)
- COMPLEX_OF_NUM_ADD
-
|- ∀m n. &m + &n = &(m + n)
- COMPLEX_OF_NUM_MUL
-
|- ∀m n. &m * &n = &(m * n)
- COMPLEX_SCALAR_LMUL
-
|- ∀k l z. k * (l * z) = k * l * z
- COMPLEX_SCALAR_LMUL_NEG
-
|- ∀k z. -(k * z) = -k * z
- COMPLEX_NEG_SCALAR_LMUL
-
|- ∀k z. k * -z = -k * z
- COMPLEX_SCALAR_LMUL_ADD
-
|- ∀k l z. (k + l) * z = k * z + l * z
- COMPLEX_SCALAR_LMUL_SUB
-
|- ∀k l z. (k − l) * z = k * z − l * z
- COMPLEX_ADD_SCALAR_LMUL
-
|- ∀k z w. k * (z + w) = k * z + k * w
- COMPLEX_SUB_SCALAR_LMUL
-
|- ∀k z w. k * (z − w) = k * z − k * w
- COMPLEX_MUL_SCALAR_LMUL2
-
|- ∀k l z w. k * z * (l * w) = k * l * (z * w)
- COMPLEX_LMUL_SCALAR_LMUL
-
|- ∀k z w. k * z * w = k * (z * w)
- COMPLEX_RMUL_SCALAR_LMUL
-
|- ∀k z w. z * (k * w) = k * (z * w)
- COMPLEX_SCALAR_LMUL_ZERO
-
|- ∀z. 0 * z = 0
- COMPLEX_ZERO_SCALAR_LMUL
-
|- ∀k. k * 0 = 0
- COMPLEX_SCALAR_LMUL_ONE
-
|- ∀z. 1 * z = z
- COMPLEX_SCALAR_LMUL_NEG1
-
|- ∀z. -1 * z = -z
- COMPLEX_DOUBLE
-
|- ∀z. z + z = 2 * z
- COMPLEX_SCALAR_LMUL_ENTIRE
-
|- ∀k z. (k * z = 0) ⇔ (k = 0) ∨ (z = 0)
- COMPLEX_EQ_SCALAR_LMUL
-
|- ∀k z w. (k * z = k * w) ⇔ (k = 0) ∨ (z = w)
- COMPLEX_SCALAR_LMUL_EQ
-
|- ∀k l z. (k * z = l * z) ⇔ (k = l) ∨ (z = 0)
- COMPLEX_SCALAR_LMUL_EQ1
-
|- ∀k z. (k * z = z) ⇔ (k = 1) ∨ (z = 0)
- COMPLEX_INV_SCALAR_LMUL
-
|- ∀k z. k ≠ 0 ∧ z ≠ 0 ⇒ (inv (k * z) = inv k * inv z)
- COMPLEX_SCALAR_LMUL_DIV2
-
|- ∀k l z w. l ≠ 0 ∧ w ≠ 0 ⇒ (k * z / (l * w) = k / l * (z / w))
- COMPLEX_SCALAR_MUL_COMM
-
|- ∀k z. k * z = z * k
- COMPLEX_SCALAR_RMUL
-
|- ∀k l z. z * k * l = z * (k * l)
- COMPLEX_SCALAR_RMUL_NEG
-
|- ∀k z. -(z * k) = z * -k
- COMPLEX_NEG_SCALAR_RMUL
-
|- ∀k z. -z * k = z * -k
- COMPLEX_SCALAR_RMUL_ADD
-
|- ∀k l z. z * (k + l) = z * k + z * l
- COMPLEX_RSCALAR_RMUL_SUB
-
|- ∀k l z. z * (k − l) = z * k − z * l
- COMPLEX_ADD_RSCALAR_RMUL
-
|- ∀k z w. (z + w) * k = z * k + w * k
- COMPLEX_SUB_SCALAR_RMUL
-
|- ∀k z w. (z − w) * k = z * k − w * k
- COMPLEX_SCALAR_RMUL_ZERO
-
|- ∀z. z * 0 = 0
- COMPLEX_ZERO_SCALAR_RMUL
-
|- ∀k. 0 * k = 0
- COMPLEX_SCALAR_RMUL_ONE
-
|- ∀z. z * 1 = z
- COMPLEX_SCALAR_RMUL_NEG1
-
|- ∀z. z * -1 = -z
- CONJ_REAL_REFL
-
|- ∀x. conj (complex_of_real x) = complex_of_real x
- CONJ_NUM_REFL
-
|- ∀n. conj (&n) = &n
- CONJ_ADD
-
|- ∀z w. conj (z + w) = conj z + conj w
- CONJ_NEG
-
|- ∀z. conj (-z) = -conj z
- CONJ_SUB
-
|- ∀z w. conj (z − w) = conj z − conj w
- CONJ_MUL
-
|- ∀z w. conj (z * w) = conj z * conj w
- CONJ_INV
-
|- ∀z. conj (inv z) = inv (conj z)
- CONJ_DIV
-
|- ∀z w. conj (z / w) = conj z / conj w
- CONJ_SCALAR_LMUL
-
|- ∀k z. conj (k * z) = k * conj z
- CONJ_CONJ
-
|- ∀z. conj (conj z) = z
- CONJ_EQ
-
|- ∀z w. (conj z = w) ⇔ (z = conj w)
- CONJ_EQ2
-
|- ∀z w. (conj z = conj w) ⇔ (z = w)
- COMPLEX_MUL_RCONJ
-
|- ∀z. conj z * z = complex_of_real (RE z pow 2 + IM z pow 2)
- CONJ_ZERO
-
|- conj 0 = 0
- MODU_POW2
-
|- ∀z. modu z pow 2 = RE z pow 2 + IM z pow 2
- RE_IM_LE_MODU
-
|- ∀z. abs (RE z) ≤ modu z ∧ abs (IM z) ≤ modu z
- MODU_POS
-
|- ∀z. 0 ≤ modu z
- COMPLEX_MUL_RCONJ1
-
|- ∀z. z * conj z = complex_of_real (modu z pow 2)
- COMPLEX_MUL_LCONJ1
-
|- ∀z. conj z * z = complex_of_real (modu z pow 2)
- MODU_NEG
-
|- ∀z. modu (-z) = modu z
- MODU_SUB
-
|- ∀z w. modu (z − w) = modu (w − z)
- MODU_CONJ
-
|- ∀z. modu (conj z) = modu z
- MODU_MUL
-
|- ∀z w. modu (z * w) = modu z * modu w
- MODU_0
-
|- modu 0 = 0
- MODU_1
-
|- modu 1 = 1
- MODU_COMPLEX_INV
-
|- ∀z. z ≠ 0 ⇒ (modu (inv z) = inv (modu z))
- MODU_DIV
-
|- ∀z w. w ≠ 0 ⇒ (modu (z / w) = modu z / modu w)
- MODU_SCALAR_LMUL
-
|- ∀k z. modu (k * z) = abs k * modu z
- MODU_REAL
-
|- ∀x. modu (complex_of_real x) = abs x
- MODU_NUM
-
|- ∀n. modu (&n) = &n
- MODU_ZERO
-
|- ∀z. (z = 0) ⇔ (modu z = 0)
- MODU_NZ
-
|- ∀z. z ≠ 0 ⇔ 0 < modu z
- MODU_CASES
-
|- ∀z. (z = 0) ∨ 0 < modu z
- RE_DIV_MODU_BOUNDS
-
|- ∀z. z ≠ 0 ⇒ -1 ≤ RE z / modu z ∧ RE z / modu z ≤ 1
- IM_DIV_MODU_BOUNDS
-
|- ∀z. z ≠ 0 ⇒ -1 ≤ IM z / modu z ∧ IM z / modu z ≤ 1
- RE_DIV_MODU_ACS_BOUNDS
-
|- ∀z. z ≠ 0 ⇒ 0 ≤ acs (RE z / modu z) ∧ acs (RE z / modu z) ≤ pi
- IM_DIV_MODU_ASN_BOUNDS
-
|- ∀z. z ≠ 0 ⇒ -(pi / 2) ≤ asn (IM z / modu z) ∧ asn (IM z / modu z) ≤ pi / 2
- RE_DIV_MODU_ACS_COS
-
|- ∀z. z ≠ 0 ⇒ (cos (acs (RE z / modu z)) = RE z / modu z)
- IM_DIV_MODU_ASN_SIN
-
|- ∀z. z ≠ 0 ⇒ (sin (asn (IM z / modu z)) = IM z / modu z)
- ARG_COS
-
|- ∀z. z ≠ 0 ⇒ (cos (arg z) = RE z / modu z)
- ARG_SIN
-
|- ∀z. z ≠ 0 ⇒ (sin (arg z) = IM z / modu z)
- RE_MODU_ARG
-
|- ∀z. RE z = modu z * cos (arg z)
- IM_MODU_ARG
-
|- ∀z. IM z = modu z * sin (arg z)
- COMPLEX_TRIANGLE
-
|- ∀z. modu z * (cos (arg z),sin (arg z)) = z
- COMPLEX_MODU_ARG_EQ
-
|- ∀z w. (z = w) ⇔ (modu z = modu w) ∧ (arg z = arg w)
- MODU_UNIT
-
|- ∀x y. modu (cos x,sin x) = 1
- COMPLEX_MUL_ARG
-
|- ∀x y. (cos x,sin x) * (cos y,sin y) = (cos (x + y),sin (x + y))
- COMPLEX_INV_ARG
-
|- ∀x. inv (cos x,sin x) = (cos (-x),sin (-x))
- COMPLEX_DIV_ARG
-
|- ∀x y. (cos x,sin x) / (cos y,sin y) = (cos (x − y),sin (x − y))
- complex_pow_def_compute
-
|- (∀z. z pow 0 = 1) ∧
(∀z n. z pow NUMERAL (BIT1 n) = z * z pow (NUMERAL (BIT1 n) − 1)) ∧
∀z n. z pow NUMERAL (BIT2 n) = z * z pow NUMERAL (BIT1 n)
- COMPLEX_POW_0
-
|- ∀n. 0 pow SUC n = 0
- COMPLEX_POW_NZ
-
|- ∀z n. z ≠ 0 ⇒ z pow n ≠ 0
- COMPLEX_POWINV
-
|- ∀z. z ≠ 0 ⇒ ∀n. inv (z pow n) = inv z pow n
- MODU_COMPLEX_POW
-
|- ∀z n. modu (z pow n) = modu z pow n
- COMPLEX_POW_ADD
-
|- ∀z m n. z pow (m + n) = z pow m * z pow n
- COMPLEX_POW_1
-
|- ∀z. z pow 1 = z
- COMPLEX_POW_2
-
|- ∀z. z pow 2 = z * z
- COMPLEX_POW_ONE
-
|- ∀n. 1 pow n = 1
- COMPLEX_POW_MUL
-
|- ∀n z w. (z * w) pow n = z pow n * w pow n
- COMPLEX_POW_INV
-
|- ∀z n. inv z pow n = inv (z pow n)
- COMPLEX_POW_DIV
-
|- ∀z w n. (z / w) pow n = z pow n / w pow n
- COMPLEX_POW_L
-
|- ∀n k z. (k * z) pow n = k pow n * z pow n
- COMPLEX_POW_ZERO
-
|- ∀n z. (z pow n = 0) ⇒ (z = 0)
- COMPLEX_POW_ZERO_EQ
-
|- ∀n z. (z pow SUC n = 0) ⇔ (z = 0)
- COMPLEX_POW_POW
-
|- ∀z m n. (z pow m) pow n = z pow (m * n)
- DE_MOIVRE_LEMMA
-
|- ∀x n. (cos x,sin x) pow n = (cos (&n * x),sin (&n * x))
- DE_MOIVRE_THM
-
|- ∀z n.
(modu z * (cos (arg z),sin (arg z))) pow n =
modu z pow n * (cos (&n * arg z),sin (&n * arg z))
- EXP_IMAGINARY
-
|- ∀x. exp (i * x) = (cos x,sin x)
- EULER_FORMULE
-
|- ∀z. modu z * exp (i * arg z) = z
- COMPLEX_EXP_ADD
-
|- ∀z w. exp (z + w) = exp z * exp w
- COMPLEX_EXP_NEG
-
|- ∀z. exp (-z) = inv (exp z)
- COMPLEX_EXP_SUB
-
|- ∀z w. exp (z − w) = exp z / exp w
- COMPLEX_EXP_N
-
|- ∀z n. exp (&n * z) = exp z pow n
- COMPLEX_EXP_N2
-
|- ∀z n. exp (&n * z) = exp z pow n
- COMPLEX_EXP_0
-
|- exp 0 = 1
- COMPLEX_EXP_NZ
-
|- ∀z. exp z ≠ 0
- COMPLEX_EXP_ADD_MUL
-
|- ∀z w. exp (z + w) * exp (-z) = exp w
- COMPLEX_EXP_NEG_MUL
-
|- ∀z. exp z * exp (-z) = 1
- COMPLEX_EXP_NEG_MUL2
-
|- ∀z. exp (-z) * exp z = 1