Library Coqtail.Complex.Cdefinitions
Definition C : Set := (prod R R).
Definition R_R_to_C (a : R) (b : R) : C := (a, b).
Delimit Scope C_scope with C.
Bind Scope C_scope with C.
Open Scope C_scope.
Definition C0 := R_R_to_C 0 0.
Definition C1 := R_R_to_C 1 0.
Definition Ci := R_R_to_C 0 1.
Notation "0" := C0.
Notation "1" := C1.
Definition Cre (z : C) : R :=
let (r1, i1) := z in
r1.
Definition Cim (z : C) : R :=
let (r1, i1) := z in
i1.
Definition Cadd (z1 : C) (z2 : C) : C :=
R_R_to_C (Cre z1 + Cre z2) (Cim z1 + Cim z2).
Definition Cmult (z1 : C) (z2 : C) : C :=
R_R_to_C (Cre z1 × Cre z2 - Cim z1 × Cim z2) (Cre z1 × Cim z2 + Cim z1 × Cre z2).
Definition Copp (z1 : C) :C :=
R_R_to_C (-Cre z1) (-Cim z1).
Definition Cinv (z1 : C) : C :=
R_R_to_C (Cre z1 / (Cre z1 × Cre z1 + Cim z1 × Cim z1)) (-Cim z1 / (Cre z1 × Cre z1 + Cim z1 × Cim z1)).
Definition Cconj (z1 : C) : C :=
R_R_to_C (Cre z1) (-Cim z1).
Definition Cnorm_sqr (z1 : C) : R :=
(Cre z1 × Cre z1 + Cim z1 × Cim z1).
Definition Cnorm (z1 : C) : R :=
(sqrt (Cnorm_sqr z1)).
Definition Cscal (lambda : R) (z : C) : C :=
R_R_to_C (lambda × Cre z) (lambda × Cim z).
Definition IRC (x : R) : C := (R_R_to_C x 0%R).
Coercion IRC : R >-> C.
Infix "+" := Cadd : C_scope.
Infix "×" := Cmult : C_scope.
Notation "- z" := (Copp z) : C_scope.
Notation "/ z" := (Cinv z) : C_scope.
Infix "`*" := Cscal (at level 0): C_scope.
Definition Cminus (c1 c2 : C) : C := c1 + - c2.
Definition Cdiv (c1 c2 : C) : C := c1 × / c2.
Infix "-" := Cminus : C_scope.
Infix "/" := Cdiv : C_scope.
Infix " '+i' " := R_R_to_C (at level 60) : C_scope.