# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Finite geometric series

#### Heather Macbeth (Jun 27 2020 at 15:30):

I would like to use the lemma

```
theorem geom_sum_mul_neg [ring α] (x : α) (n : ℕ) : (geom_series x n) * (1 - x) = 1 - x ^ n
```

from algebra.geom_sum, but in the "reflected" form

```
(1 -x) * (geom_series x n) = 1 - x ^ n
```

Is there a slick way to get this, maybe using that `1`

and `x`

commute? Or do I truly need to re-prove this lemma and all the lemmas it depends on (`geom_sum_mul`

, `geom_sum₂_mul_comm`

, `geom_sum₂_mul_add`

, ...) in reflected form?

#### Jalex Stark (Jun 27 2020 at 15:34):

if you're writing a tactic mode proof, you can `have`

it and then `rw mul_comm at`

it

#### Heather Macbeth (Jun 27 2020 at 15:35):

This is a possibly non-commutative ring

#### Jalex Stark (Jun 27 2020 at 15:35):

thanks, maybe I forgot which stream I was in :)

#### Jalex Stark (Jun 27 2020 at 15:37):

hmm you could have this as a theorem about the polynomial ring $\Z[x]$

#### Bhavik Mehta (Jun 27 2020 at 15:37):

Could you show `x * geom_series x n = geom_series x n * x`

(using `x^n * x = x * x^n`

) and then use distributivity perhaps?

#### Reid Barton (Jun 27 2020 at 15:37):

Maybe we need some `big_operators`

lemmas about `commute`

#### Heather Macbeth (Jun 27 2020 at 15:42):

OK, for now I will just add reflected versions of a bunch of lemmas to `algebra.geom_sum`

; hopefully Bhavik's idea will reduce my pain.

#### Heather Macbeth (Jun 27 2020 at 15:42):

Looks like the elegant ways also require a lot of work .. so someone else can do it later.

#### Jalex Stark (Jun 27 2020 at 15:51):

This depends on #3197, which should be merged soon.

```
import tactic
variables (α R : Type*) [ring R] (s : finset α)
open_locale big_operators
open finset
lemma mul_sum_comm (f : α → R) (a : R) (ha : ∀ x ∈ s, a * f x = f x * a) :
a * ∑ x in s, f x = (∑ x in s, f x) * a :=
sum_induction f (λ r, a * r = r * a)
(λ _ _ hb hc, by rw [mul_add, add_mul, hb, hc]) (by simp) ha
```

#### Reid Barton (Jun 27 2020 at 15:52):

There is already `commute`

which handles the parts of this other than the induction on the sum

#### Heather Macbeth (Jun 27 2020 at 15:53):

Heather Macbeth said:

Looks like the elegant ways also require a lot of work .. so someone else can do it later.

Wait, is this becoming "someone else can do it right now"? :)

#### Jalex Stark (Jun 27 2020 at 15:55):

mm how much more are you asking to be done? this was just meant to help prove that `x`

commutes with `geom_series x n`

#### Heather Macbeth (Jun 27 2020 at 15:57):

This counts as an elegant way, as far as I am concerned.

#### Heather Macbeth (Jun 27 2020 at 15:58):

By the way, is it too late to add that lemma to #3197?

#### Jalex Stark (Jun 27 2020 at 15:59):

I guess not, I'm working to make it depend on `commute`

as Reid suggested

#### Jalex Stark (Jun 27 2020 at 15:59):

(I think #3197 is in a state where it will be accepted next time a reviewer notices that it has passed the linter)

#### Jalex Stark (Jun 27 2020 at 16:14):

```
import tactic
variables {α R : Type*} [ring R] {s : finset α}
open_locale big_operators
open finset
lemma commute_add (a b c : R) (hb : commute a b) (hc : commute a c) :
commute a (b + c) :=
begin
unfold commute, unfold semiconj_by,
rw [mul_add, add_mul, hb.eq, hc.eq],
end
lemma commute_zero (a : R) : commute a 0 := by simp
lemma commute_sum (f : α → R) (a : R) (ha : ∀ x ∈ s, commute a (f x)) :
commute a (∑ x in s, f x) :=
sum_induction _ _ (commute_add a) (commute_zero a) ha
```

#### Jalex Stark (Jun 27 2020 at 16:17):

do you have any need for

```
def commutator (a b : R) : Prop := a * b - b * a
```

#### Reid Barton (Jun 27 2020 at 16:17):

First two are `commute.add_right`

and `commute.zero_right`

.

#### Jalex Stark (Jun 27 2020 at 16:17):

mm maybe I should have tried `library_search`

after my eyeball-search failed

#### Jalex Stark (Jun 27 2020 at 16:18):

should commute_sum go in `algebra.big_operators`

? `commute`

? somewhere else?

#### Reid Barton (Jun 27 2020 at 16:18):

@Yury G. Kudryashov @Chris Hughes ?

#### Chris Hughes (Jun 27 2020 at 16:48):

I would put it in `commute`

. Probably worth proving that the set of elements that commute with `a`

form a subring, and perhaps that the ring generated by a set of elements that commute is commutative.

#### Yury G. Kudryashov (Jun 27 2020 at 18:04):

`commute`

does not depend on `finset`

anymore.

#### Yury G. Kudryashov (Jun 27 2020 at 18:05):

We can define `subsemiring.centralizer`

, then say something about `sum_mem`

.

#### Yury G. Kudryashov (Jun 27 2020 at 18:05):

Or just put `commute.sum_right`

, `commute.sum_left`

, and `commute.sum_sum`

into `algebra.big_operators`

.

#### David Wärn (Jun 27 2020 at 18:46):

Another way of thinking about this: the desired result is `algebra.geom_sum`

in the opposite ring docs#opposite.ring

#### Johan Commelin (Jun 27 2020 at 18:53):

Nice! (-;

#### Reid Barton (Jun 27 2020 at 19:47):

Do we have a lemma that says that powers in the opposite ring are the same as powers in the original ring though?

#### David Wärn (Jun 27 2020 at 21:10):

I don't think so. Should we? Note that this is really a result about powers in the opposite monoid

#### Bhavik Mehta (Jun 27 2020 at 22:08):

I think that lemma should exist, since there's lemmas for `mul`

and `add`

so it seems odd to make users of the API implement the `pow`

version themselves

#### David Wärn (Jun 28 2020 at 08:58):

#### Heather Macbeth (Jun 28 2020 at 12:16):

Oh, sorry, it's also in #3210 !

#### Heather Macbeth (Jun 28 2020 at 20:29):

By the way, here is my proof (from #3210) of the original fact.

```
lemma mul_geom_sum [ring α] (x : α) (n : ℕ) :
(x - 1) * (geom_series x n)= x ^ n - 1 :=
begin
refine (op_inj_iff _ _).mp _,
rw [op_mul, op_geom_series],
have h1 : op x - 1 = op (x - 1) :=
by rw [← op_one, sub_eq_add_neg, ← op_neg, ← op_add, sub_eq_add_neg],
rw ← h1,
have h2 : op x ^ n - op 1 = op (x ^ n - 1) :=
by { rw [sub_eq_add_neg, ← op_neg, ← op_pow, ← op_add], refl },
rw ← h2,
exact geom_sum_mul _ _,
end
```

Could this be automated? I request a tactic `oppify`

!

#### Kevin Buzzard (Jun 28 2020 at 20:50):

Is this a job for `norm_cast`

?

#### Heather Macbeth (Jun 28 2020 at 20:52):

I have not used `norm_cast`

, but the principle looks very similar. Would it work right now, or does someone need to rewrite the `norm_cast`

tactic to include this as a suitable cast?

#### Kevin Buzzard (Jun 28 2020 at 20:55):

You have to tag all the lemmas like `op_add`

and `op_one`

with @[norm_cast] and then you apply it and hope.

#### Kevin Buzzard (Jun 28 2020 at 20:57):

I don't know what `op`

is so I'm not 100% sure what I'm talking about, but here's an example of it all working with the coercion from the reals to the complexes. I tag a bunch of things `norm_cast`

and then the tactic can prove "obvious" stuff. https://github.com/ImperialCollegeLondon/complex-number-game/blob/master/src/complex/Level_01_of_real.lean#L161

#### David Wärn (Jun 28 2020 at 20:57):

I think this is a job for `simp`

. There's a missing lemma for subtraction

```
@[simp] lemma op_sub [ring α] (x y : α) : op (x - y) = op x - op y := rfl
lemma mul_geom_sum [ring α] (x : α) (n : ℕ) :
(x - 1) * (geom_series x n)= x ^ n - 1 :=
begin
rw ←op_inj_iff,
simpa [op_geom_series] using geom_sum_mul (op x) n,
end
```

#### Kevin Buzzard (Jun 28 2020 at 20:59):

If `simp`

can manage it, then great! `norm_cast`

was developed because of Mario's insistence that `simp`

was not a great tool for this kind of problem in general.

#### Heather Macbeth (Jun 28 2020 at 23:03):

Works beautifully, thank you @David Wärn !

#### Mario Carneiro (Jun 29 2020 at 03:01):

Kevin Buzzard said:

If

`simp`

can manage it, then great!`norm_cast`

was developed because of Mario's insistence that`simp`

was not a great tool for this kind of problem in general.

To clarify, `simp`

is good if what you want to do is push all the coercions to the leaves, for example if you want to prove a theorem about `nat`

by applying `int.coe_nat_inj`

and then use `simp`

to put an up arrow on every variable. If you want to do the opposite, pulling all the up arrows to the top level so they can be eliminated (like if we wanted to do the reverse of the nat -> int process just described), then `simp`

will fight you because you are going uphill relative to simp normal form

Last updated: May 07 2021 at 21:10 UTC