Stream: math-comp users

Topic: Complex number equality


view this post on Zulip Florent Hivert (Oct 25 2021 at 21:52):

Hi there ! I didn't find the following lemma

Lemma eq_Re_Im (T : numClosedFieldType) (x y : T) :
  (x == y) = ('Re x == 'Re y) && ('Im x == 'Im y).
Proof.
apply/eqP/andP => [->//|[/eqP eqRe /eqP eqIm]].
by rewrite (Crect x) eqRe eqIm -Crect.
Qed.

Did I miss something ? Should I throw yet another PR ? Any suggestion of better name ?

view this post on Zulip Cyril Cohen (Oct 26 2021 at 08:19):

Hi, I recently noticed it's absence and I was actually making a PR for it along with other missing lemmas.

view this post on Zulip Cyril Cohen (Oct 26 2021 at 09:08):

math-comp/math-comp#818

view this post on Zulip Florent Hivert (Oct 26 2021 at 12:01):

Excellent ! I might have some more lemmas to suggest...

view this post on Zulip Cyril Cohen (Oct 26 2021 at 12:14):

Florent Hivert said:

Excellent ! I might have some more lemmas to suggest...

please do

view this post on Zulip Reynald Affeldt (Oct 26 2021 at 12:18):

didn’t @Marie Kerjean produce many such lemmas for holomorphy?

view this post on Zulip Marie Kerjean (Oct 26 2021 at 14:08):

Reynald Affeldt said:

didn’t Marie Kerjean produce many such lemmas for holomorphy?

Yes, here among other lemmas, but with equality in Prop and other mc-analysis things.

view this post on Zulip Cyril Cohen (Oct 26 2021 at 14:10):

Marie Kerjean said:

Reynald Affeldt said:

didn’t Marie Kerjean produce many such lemmas for holomorphy?

Yes, here among other lemmas, but with equality in Prop and other mc-analysis things.

Also it is not for a numClosedFieldType but for R[i].


Last updated: Feb 08 2023 at 07:02 UTC