Sum over fin 2

Stream: new members

[Eloi]

I am defining concrete subgroups of SL2(Z) by imposing conditions on the entries of matrices.

After some work, i have reduced the mul_mem' condition to (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0, but I don't know how to make progress with finite sums.

What can I do in this minimal example?

import data.fin
import data.matrix.basic

--import algebra.big_operators


variables {A B: matrix (fin 2) (fin 2) ℤ}

open_locale big_operators
lemma lem : (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0:=
    begin
        dsimp,
        rw matrix.mul,
        simp only,
        rw matrix.dot_product,

--  I'm stuck here
        --  The goal is
        --     ⊢ ∑ (i : fin 2), A 1 i * B i 0
        --      = A 1 0 * B 0 0 + A 1 1 * B 1 0
        sorry
    end

Thanks

[Kenny Lau]

import data.fin
import data.matrix.basic

--import algebra.big_operators

variables {A B : matrix (fin 2) (fin 2) ℤ}

open_locale big_operators

lemma lem : (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 :=
show (A 1 0 * B 0 0) + (A 1 1 * B 1 0 + 0) = _, by rw add_zero

[Kenny Lau]

defeqs FTW

[Eloi]

Wow awesome!

Thanks!