ssreflect - Re: [ssreflect] bigop in abelian subsets

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] bigop in abelian subsets

From: Florent Hivert <>
To: Georges Gonthier <>
Cc: "" <>, Thibaut Benjamin <>
Subject: Re: [ssreflect] bigop in abelian subsets
Date: Tue, 19 Apr 2016 13:52:16 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
Ironport-phdr: 9a23:/XlXQRdnatAdTFmYEJvkPaVvlGMj4u6mDksu8pMizoh2WeGdxc6yYR7h7PlgxGXEQZ/co6odzbGG4+a+BSdcu96oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDivcOPKFkSzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzayXYbSGobiVJnBA7Z7BD3RN+lvSz8qup81TOyOMz9V7cvXjq+qaxsTUm7pj0AMmsX9GbNh8psxIJavh+7u1Qr7YrTeoyTKLxef73QZ88yQXBAGMhLAX8SSrigZpcCWrJSdd1TqJPw8h5X9UOz

Dear Georges,

On Tue, Apr 19, 2016 at 09:41:35AM +0000, Georges Gonthier wrote:
[...]
> - To avoid these issues I'd recommend keeping to a more declarative style
> and explicitly writing out the main sums involved in the proof. You can look
> at the proof of Gaschütz' theorem in finmodule for an example of that style.

Thanks a lot for all these suggestions ! We'll try it !

Cheers,

Florent

[ssreflect] bigop in abelian subsets, Florent Hivert, 04/18/2016
- Re: [ssreflect] bigop in abelian subsets, Emilio Jesús Gallego Arias, 04/18/2016
  - Re: [ssreflect] bigop in abelian subsets, Emilio Jesús Gallego Arias, 04/18/2016
- RE: [ssreflect] bigop in abelian subsets, Georges Gonthier, 04/18/2016
  - RE: [ssreflect] bigop in abelian subsets, Georges Gonthier, 04/19/2016
    - Re: [ssreflect] bigop in abelian subsets, Florent Hivert, 04/19/2016

List archive

Re: [ssreflect] bigop in abelian subsets