Library C_complements

This file is a complement of complex.v of SSReflect library. In particular it contains lemmas to facilitate the correspondence between a real number and a complex number with a null imaginary part.


Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Section prelemme.

Variable R : rcfType.
Local Notation C := (complex R).

Open Scope ring_scope.

Lemma Im0 (a : C) : a \is Num.real -> Im a = 0.

Lemma Re_ge0 (a : C) : a \is Num.real -> (0 <= Re a) = (0 <= a).

Lemma Re_gt0 (a : C) : a \is Num.real -> (0 < Re a) = (0 < a).

Lemma real_Re_eq0 (x : C) : x \is Num.real -> (Re x == 0) = (x == 0).

Lemma real_lecE (x y : C) : x \is Num.real -> y \is Num.real ->
   (x <= y) = (Re x <= Re y).

Lemma real_ltcE (x y : C) : x \is Num.real -> y \is Num.real ->
   (x < y) = (Re x < Re y).

Lemma ReK (a : C) : a \is Num.real -> (Re a)%:C = a.

Lemma ReM (a b : C) : Re (a * b) = Re a * Re b - Im a * Im b.

Lemma real_ReM (a b : C) : a\is Num.real -> b \is Num.real ->
  Re ( a * b) = Re a * Re b.

Lemma real_ReX (a : C) n : a\is Num.real -> Re (a ^+ n) = (Re a) ^+ n.

Lemma real_ReV (a : C) : a \is Num.real -> Re (a^-1) = (Re a)^-1.

Lemma normc_real (x : R) : `|x%:C| = `|x|%:C.

Lemma Re_nat (n : nat) : Re (n%:R : C) = (n%:R : R).

Lemma natC (n : nat) : ((n%:R : R)%:C)=(n%:R : C).

End prelemme.

This page has been generated by coqdoc