Open
Description
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.
Metadata
Metadata
Assignees
Labels
No labels