Ssreflect Users Discussion List

[Vincent Siles <>]

Fair enough :)

Thanks !
Vincent

2012/2/2 Pierre-Yves Strub <>:
> Hi,
>
> Parameter R : comRingType.
>
>
> Definition multi_linear (m n:nat) (f: 'M[R]_(m,n) -> R) :=
>  forall (A B C: 'M[R]_(m,n)) (i: 'I_m) (b c: R),
>       row i A = b *: row i B + c *: row i C ->
>       row' i B = row' i A ->
>       row' i C = row' i A -> f A = b * f B + c * f C.
>
> Lemma multi_linear0 (m n: nat) (f: 'M[R]_(m, n) -> R) :
>
>  multi_linear f -> f 0 = 0.
> Proof. Admitted.
>
> Goal false.
> Proof.
>  have: (@multi_linear 0 0 (fun _ => 1)) by move=> ??? [].
>  by move/multi_linear0=> /eqP; rewrite oner_eq0.
> Qed.
>
> Pierre-Yves.
>
>
> On 02/02/2012 02:50 PM, Vincent Siles wrote:
>>
>> Hi there,
>>
>> I'm playing a bit with multi-linear maps using the following definition:
>>
>> Definition multi_linear (m n:nat) (f: 'M[R]_(m,n) ->  R) :=
>>   forall (A B C: 'M[R]_(m,n)) (i: 'I_m) (b c: R),
>>        row i A = b *: row i B + c *: row i C ->
>>        row' i B = row' i A ->
>>        row' i C = row' i A ->  f A = b * f B + c * f C.
>>
>> extracted from multilinear_determinant.
>>
>> Using this formula it easy to prove that
>>
>> Lemma multi_linear0 (m n: nat) (f: 'M[R]_(1 + m,n) ->  R) :
>>   multi_linear f ->  f 0 = 0.
>>
>> I wonder if it is possible (or true, I'm not sure) to generalize this
>> result and
>> prove that it also holds for any f : 'M[R]_(0,n) ->  R ?
>>
>> I know that "0 sized" matrices have weird properties, so I'm unsure if
>> this is
>> true or not.
>>
>> Best,
>> Vincent
>
>