Florent Hivert (Oct 25 2021 at 21:52): 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 ?
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.
Cyril Cohen (Oct 26 2021 at 09:08): Florent Hivert (Oct 26 2021 at 12:01):Excellent ! I might have some more lemmas to suggest...
Cyril Cohen (Oct 26 2021 at 12:14):Florent Hivert said:
Excellent ! I might have some more lemmas to suggest...
please do
Reynald Affeldt (Oct 26 2021 at 12:18):didn’t @Marie Kerjean produce many such lemmas for holomorphy?
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.
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
Propand other mc-analysis things.
Also it is not for a numClosedFieldType but for R[i].
Last updated: Feb 08 2023 at 07:02 UTC