Ssreflect Users Discussion List

Thanks.  One more question.

Is there some hidden lemma that says

forall (R : ringType) (A : lalgType R) (k : R) (x : A),
  k *: x = k%:A * x.

somewhere that I just cannot find?

On Mon, 9 May 2011, Laurent Théry wrote:

> On 05/09/2011 01:53 PM,  wrote:
> > If f : 'End(L), then (fun_of_lapp f) is linear and hence addtitive, so I 
> > would have expected [additive of f] to type check; however there appears to 
> > be no canonical additive structure for 'End(L).  Is this the case?
> >
> > I'm trying to map a linear transformation over a polynomial, so f isn't an 
> > rmorphism (it is only an rmorphism on a subalgebra of L), but it ought to 
> > be additive.
>
> Overlook, corrected in the new commit.
>
> --
> Laurent

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''