## Stream: new members

### Topic: iterating over subscripts & generalizing products

#### Alena Gusakov (Jun 24 2020 at 20:24):

So if I want to prove a statement like (a₁ * a₂ * ... * a_n)⁻¹ = a_n⁻¹ *...*a₂⁻¹ *a₁⁻¹, how would I write it out?

#### Jalex Stark (Jun 24 2020 at 20:25):

check out docs#finset.prod

#### Aniruddh Agarwal (Jun 24 2020 at 20:26):

Jalex beat me to it :P

#### Jalex Stark (Jun 24 2020 at 20:26):

it has many useful lemmas :)

#### Jalex Stark (Jun 24 2020 at 20:27):

you can win the race next time if you use the linkifier

#### Jalex Stark (Jun 24 2020 at 20:30):

ah this won't work, finset.prod is about commutative multiplication

docs#list.prod

#### Alena Gusakov (Jun 24 2020 at 20:34):

Yeah I'm trying to prove it

#### Alena Gusakov (Jun 24 2020 at 20:35):

list.prod takes care of the product, but I still don't get how to iterate over subscripts. Is there some list constructor for that?

#### Jalex Stark (Jun 24 2020 at 20:36):

(list.map a (list.range n)), where (a : ℕ → G) and G is your group. I don't think we have something like python list comprehensions, if that's what you're asking

#### Yakov Pechersky (Jun 24 2020 at 20:38):

example {a b c d : ℝ} : (a * b * c * d)⁻¹ = d⁻¹ * c⁻¹ * b⁻¹ * a⁻¹ :=
by { simp [mul_inv', mul_assoc] }


#### Alena Gusakov (Jun 24 2020 at 20:38):

I don't know exactly how to phrase my question haha sorry, though I do think what you gave me is what I'm looking for

#### Alena Gusakov (Jun 24 2020 at 20:39):

I'm trying to solve it for all n so it's an induction type proof

#### Alena Gusakov (Jun 24 2020 at 20:39):

Gonna have to tinker with the list.map thing

#### Yakov Pechersky (Jun 24 2020 at 20:40):

Do you have an example of the place you need to do it at in a #mwe?

#### Alena Gusakov (Jun 24 2020 at 20:41):

Like the proof itself? It's just an exercise, I'm trying to go through Dummit and Foote and prove basic stuff

#### Jalex Stark (Jun 24 2020 at 20:42):

I think this is mathematically the right statement

import tactic

variables (G : Type*) [group G] (n : ℕ) (a : ℕ → G)

example :
(list.map a (list.range n)).prod⁻¹ = (list.map (λ x, (a x)⁻¹) (list.range n).reverse).prod :=
begin
sorry
end


#### Yakov Pechersky (Jun 24 2020 at 20:42):

From what I've learned on this channel is that statements about general a_1, ... a_i, ..., a_n aren't very Lean friendly

#### Alena Gusakov (Jun 24 2020 at 20:43):

Oof okay, good to know

#### Yakov Pechersky (Jun 24 2020 at 20:43):

I could be totally wrong though.

#### Jalex Stark (Jun 24 2020 at 20:44):

i think working with a list is slightly harder than working with a finset, but i think working with lists in lean is not much more awkward than working with lists in haskell

#### Alex J. Best (Jun 24 2020 at 20:44):

Its probably best when doing problems like this to use a list L and do induction on L instead of indices directly.

#### Alena Gusakov (Jun 24 2020 at 20:45):

Oh no this one is gonna be really tedious

#### Alena Gusakov (Jun 24 2020 at 20:45):

@Alex J. Best so like, append elements?

#### Alena Gusakov (Jun 24 2020 at 20:46):

I don't really know how that would look

#### Jalex Stark (Jun 24 2020 at 20:46):

I think Alex is suggesting that the statement you want to prove is literally docs#inv_prod

Ahh okay I see

#### Jalex Stark (Jun 24 2020 at 20:48):

lemma inv_prod {G : Type*} [group G] (l : list G) :
(l.prod)⁻¹ = (list.map (λ x , x⁻¹) l.reverse).prod


#### Alex J. Best (Jun 24 2020 at 20:48):

So yeah the lemma is in mathlib, but you should totally try and prove it still!
Yes, lists are defined as an inductive type, so the empty list is a list, and if L is a list and a is an element, then a :: L is also a list, this notation means append a to the start of L, so a :: [b,c] is [a, b, c], or this is a :: b :: c :: [].
Because its an inductive type doing the induction on lists of different lengths works well, just call induction L to split into these two cases the empty list and a :: L for some a  and L.

#### Alena Gusakov (Jun 24 2020 at 20:50):

In this case would it be a good idea to start with an a :: [] appended already since the statement doesn't really mean anything on an empty list? Or is that a perfectly valid thing to do?

#### Jalex Stark (Jun 24 2020 at 20:51):

list.prod is defined for the empty list

#### Jalex Stark (Jun 24 2020 at 20:51):

and your theorem is true for it

Okay yeah fair

#### Alex J. Best (Jun 24 2020 at 20:51):

Well the advantage of the empty list is that a lot of statements are trivial for that, compared to a :: [], [].prod =1  for example.
BTW the setup for induction would be like this:

lemma inv_prod {α : Type*} [group α] (L : list α) : L.prod⁻¹ = (L.reverse.map (λ x, x⁻¹)).prod :=
begin
induction L,
{ sorry },
{ sorry },
end


#### Alena Gusakov (Jun 24 2020 at 20:52):

Gotcha, thank you!

#### Jalex Stark (Jun 24 2020 at 20:55):

If you want to start from a black box and work backwards, simp can do all the bits, and squeeze_simp will tell you what simp found

import tactic

lemma inv_prod {G : Type*} [group G] (l : list G) :
(list.prod l)⁻¹ = (list.map (λ x, x⁻¹) l.reverse).prod :=
begin
induction l with hd tl h,
squeeze_simp,
squeeze_simp [h],
end


#### Yakov Pechersky (Jun 24 2020 at 20:55):

fin version seems more natural to me

import tactic
import algebra.big_operators
import data.fintype.card

open_locale big_operators

variables (G : Type*) [comm_group G] (n : ℕ) (a : fin n.succ → G)

example :
(∏ i, (a i))⁻¹ = ∏ i, (a i)⁻¹ :=
begin
induction n with k hk,
simp,
simp [fin.prod_univ_succ, mul_inv],
end


#### Yakov Pechersky (Jun 24 2020 at 20:57):

It doesn't have the reversal going on, though

#### Jalex Stark (Jun 24 2020 at 20:57):

you're proving an easier lemma

Yeah, using comm

#### Jalex Stark (Jun 24 2020 at 20:58):

you're taking an unordered product of elements of a commutative group

#### Yakov Pechersky (Jun 24 2020 at 20:58):

And Prod requires comm_monoid

#### Jalex Stark (Jun 24 2020 at 20:59):

right, that's why we were not using the big operator stuff

Gotcha

#### Jalex Stark (Jun 24 2020 at 20:59):

it might not be hard to define big operators over lists, but afaik nobody has done it

#### Bryan Gin-ge Chen (Jun 24 2020 at 21:06):

Patrick is fond of recommending the paper on Coq's big operator library: https://hal.inria.fr/inria-00331193/PDF/main.pdf

#### Jalex Stark (Jun 24 2020 at 21:44):

This works for doing list.prod through notation (though there's an embarrassingly simple sorry)

import tactic

localized "notation ∏ binders  in  l ,  r:(scoped:67 f, (list.map f l).prod) := r" in big_list_prod

variables (G : Type*) [comm_group G] (n : ℕ) (a : ℕ → G)

open list
open_locale big_list_prod

@[simp]
lemma range_zero : range 0 = nil := rfl

@[simp]
lemma range_succ (n : ℕ) : range n.succ = n :: range n := sorry

example (n : ℕ) :
∏ i in range n, (a i)⁻¹ = (∏ i in (range n).reverse, a i)⁻¹ :=
begin
induction n with d hd,
{ simp },
simp [hd],
end


Last updated: May 15 2021 at 02:11 UTC