# Zulip Chat Archive

## 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

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

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

that looks like the theorem alena asked about

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

#### 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

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

Ahh okay I see

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

here's the statement, for anyone that doesn't follow the link

```
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

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

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

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

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

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

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: Dec 20 2023 at 11:08 UTC