Ssreflect Users Discussion List

[Cyril Cohen <>]

On 01/06/2015 08:13, bertot wrote:
> In ssralg, there is a theorem named exprM with the following statement.
> 
> Lemma exprM x m n : x ^+ (m * n) = x ^+ m ^+ n.
> 
> In complex, there is a theorem named exprM with the following statement.
> 
> Lemma exprM (a b : R) : (a * b) ^+ 2 = a ^+ 2 * b ^+ 2.
> 
> I know that complex is not part of an official distribution yet, but
> still this naming scheme is
> not consistent.  I suggest that  the latter should be named
> 
> expMn

That's a critical mistake of mine ;)

I think a way better name is sqrM, because it is not about exponential
in general but about squares,

However it looks like a useless theorem, since it can be subsumed by exprMn.

-- 
Cyril