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