## Stream: new members

### Topic: Sum over fin 2

#### Eloi (Jul 14 2020 at 11:00):

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 (Jul 14 2020 at 11:04):

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


defeqs FTW

#### Eloi (Jul 14 2020 at 11:10):

Wow awesome!

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC