Zulip Chat Archive

Stream: new members

Topic: Sum over fin 2


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 14 2020 at 11:04):

defeqs FTW

view this post on Zulip Eloi (Jul 14 2020 at 11:10):

Wow awesome!

Thanks!


Last updated: May 11 2021 at 00:31 UTC