# Zulip Chat Archive

## Stream: general

### Topic: basic struggles

#### Johan Commelin (Aug 07 2018 at 05:45):

I find myself struggling with things that are extremely math-trivial. If I have a goal of the form `a = b`

, how do I turn that into `a * c = b * c`

? (Assume that `a b c : R`

and `[comm_ring R]`

.)

#### Simon Hudon (Aug 07 2018 at 05:53):

Have you tried `mul_right_cancel_iff`

?

#### Johan Commelin (Aug 07 2018 at 05:57):

Hmmm, I only need the easy implication, for which I don't need a cancellative instance.

#### Johan Commelin (Aug 07 2018 at 05:57):

And in fact I don't have an instance of cancellative semiblabla... :sad:

#### Simon Hudon (Aug 07 2018 at 06:25):

Ok, I think I see the issue. If `R`

was a multiplicative group, you'd have a `left_cancel_semigroup`

for free. As it is, your statement is not true I think because rings don't have a multiplicative inverse for every non-zero element.

#### Simon Hudon (Aug 07 2018 at 06:26):

If you had a field though ...

#### Simon Hudon (Aug 07 2018 at 06:26):

Can you choose your `c`

so that it has an inverse?

#### Johan Commelin (Aug 07 2018 at 06:26):

Hmmz, sorry, I've been brainfarting...

#### Johan Commelin (Aug 07 2018 at 06:27):

My `c`

has an inverse

#### Simon Hudon (Aug 07 2018 at 06:27):

How rude! :)

#### Johan Commelin (Aug 07 2018 at 06:28):

I'll copy-paste my goal.

#### Johan Commelin (Aug 07 2018 at 06:28):

(witt_polynomial n - map₂ witt_polynomial C (finset.sum finset.univ (λ (i : fin n), ↑p ^ i.val * X_in_terms_of_W (i.val) ^ p ^ (n - i.val)))) * C (1 / ↑p ^ (n + 1)) = X n

#### Johan Commelin (Aug 07 2018 at 06:28):

So you see that there is this term `C (1 / _)`

.

#### Johan Commelin (Aug 07 2018 at 06:28):

I would like to move it to the other side.

#### Johan Commelin (Aug 07 2018 at 06:29):

This goal has been misbehaving quite a lot, lately.

#### Simon Hudon (Aug 07 2018 at 06:31):

What is the statement that `C (1 / _)`

has an inverse like?

(it does look pretty hairy)

#### Johan Commelin (Aug 07 2018 at 06:34):

Well `1 / _`

has an inverse in `rat`

. And `C`

is a ring hom. So it maps inverses to inverses.

#### Simon Hudon (Aug 07 2018 at 06:38):

So in short, `C _`

is the inverse `C (1 / _)`

I assume. It is surprisingly hard to sneak in I realize. Any chance `C`

has an inverse? Then you could transform your goal from `R`

to `rat`

just long enough to play with the inverse.

#### Simon Hudon (Aug 07 2018 at 06:39):

(That's probably a long shot: if you had that inverse of C, `R`

would probably be a field)

#### Johan Commelin (Aug 07 2018 at 06:39):

No, `C`

is the function `R \to mv_polynomial Xs R`

that takes a ring element to the constant polynomial.

#### Simon Hudon (Aug 07 2018 at 06:40):

I'm starting to think your assumptions are not strong enough for what you're trying to do

#### Johan Commelin (Aug 07 2018 at 06:40):

Ok, so `rat`

is a field, therefore `p^(n+1)`

has an inverse (it is nonzero). Now I apply `C`

to `p^(n+1)`

and I get a crazy element of some ring, and it will still have an inverse.

#### Johan Commelin (Aug 07 2018 at 06:41):

So I want to multiply both sides with `C (p^(n+1))`

.

#### Mario Carneiro (Aug 07 2018 at 06:42):

you are thinking backwards

#### Simon Hudon (Aug 07 2018 at 06:42):

What if you multiply by `C 1`

on the right

#### Mario Carneiro (Aug 07 2018 at 06:42):

you want to multiply some equation that will be your new goal by `C (1 / ↑p ^ (n + 1))`

#### Johan Commelin (Aug 07 2018 at 06:43):

Right

#### Johan Commelin (Aug 07 2018 at 06:44):

So I use suffices?

#### Simon Hudon (Aug 07 2018 at 06:44):

... and then decompose it to `C (x * 1/x)`

and then `C x * C (1/x)`

#### Mario Carneiro (Aug 07 2018 at 06:45):

Here's a trick: `rw (_ : _ - _ = X n * C (p ^ (n + 1)))), {simp}`

#### Mario Carneiro (Aug 07 2018 at 06:45):

(maybe `simp`

won't kill that goal, you may need to do some more careful rewrites, but it should still be relatively easy)

#### Simon Hudon (Aug 07 2018 at 06:45):

Whaaaa?

#### Mario Carneiro (Aug 07 2018 at 06:47):

there should be a simp lemma `C(1/x) = 1/C x`

#### Mario Carneiro (Aug 07 2018 at 06:47):

then `simp`

will kill the goal

#### Johan Commelin (Aug 07 2018 at 06:51):

Too bad:

failed to synthesize type class instance for ⊢ has_sub (mv_polynomial ℕ ℕ)

#### Johan Commelin (Aug 07 2018 at 06:51):

It didn't figure out the base ring...

#### Mario Carneiro (Aug 07 2018 at 06:54):

You have to add a type ascription

#### Mario Carneiro (Aug 07 2018 at 06:55):

or fill it in a bit more, `witt_polynomial n - _ = ...`

#### Johan Commelin (Aug 07 2018 at 07:21):

@Mario Carneiro I'm not sure if `1/C x`

makes sense? There is no division in the polynomial ring, right?

#### Johan Commelin (Aug 07 2018 at 07:22):

Or maybe there is, in the sense of Euclidean domains... but that is not what we want here.

#### Mario Carneiro (Aug 07 2018 at 07:22):

Oh, I see... `C x`

is a unit of the ring

#### Mario Carneiro (Aug 07 2018 at 07:24):

maybe this is why I thought `C_mul`

was not a good simp lemma

Last updated: May 16 2021 at 05:21 UTC