Open SnarkBoojum opened 2 years ago
Trying to play with trigonometry formulas, I found the following lemmas on complex numbers useful:
Lemma conjRe: forall z: CC, Re z^* = Re z. Proof. by move=> [a b]. Qed. Lemma conjIm: forall z: CC, Im z^* = -Im z. Proof. by move=> [a b]. Qed. Lemma mulRe: forall w z: CC, Re (w * z) = (Re w) * (Re z) - (Im w) * (Im z). Proof. by move=> [a b] [c d]. Qed. Lemma mulIm: forall w z: CC, Im (w * z) = (Re w) * (Im z) + (Im w) * (Re z). Proof. by move=> [a b] [c d]. Qed.
Trying to play with trigonometry formulas, I found the following lemmas on complex numbers useful: