# Zulip Chat Archive

## Stream: maths

### Topic: integer multiplication well-defined

#### Kevin Buzzard (Jan 06 2020 at 04:42):

On the plane to Pittsburgh I was idly thinking about "the integer game". If one defines the integers as being $\mathbb{N}^2/\sim$ with $\sim$ the usual equivalence relation, then everything goes pretty smoothly until you want to prove multiplication is well-defined, and then you end up with

i j k l m n p q : ℕ, h1 : (i, j) ≈ (m, n), h2 : (k, l) ≈ (p, q) ⊢ (i * k + j * l, i * l + k * j) ≈ (m * p + n * q, m * q + p * n)

which turns into this:

1 goal i j k l m n p q : ℕ, h2 : k + q = p + l, h1 : i + n = m + j ⊢ i * k + j * l + (m * q + p * n) = m * p + n * q + (i * l + k * j)

which took me about 9 lines of `calc`

:-/ (start by applying `add_left_inj`

and then alternate lines of `ring`

and `rw hi`

). Am I right in thinking that there's no automation which will do this? There is probably a one-line "miracle proof" if you figure out some auxiliary ring theory equality. Modulo this, the proof that the integers are a ring comes out quite nicely.

#### Kenny Lau (Jan 06 2020 at 04:53):

maybe don't use equivalence relation

#### Kenny Lau (Jan 06 2020 at 04:54):

use `quot`

and `r (i,j) (i+1,j+1)`

#### Kevin Buzzard (Jan 06 2020 at 04:55):

Here's what I did: https://gist.github.com/kbuzzard/e86eb3788caab340d5c40732de23d131

#### Kevin Buzzard (Jan 06 2020 at 04:58):

I want to make it look familiar to mathematicians. There will be a one-line proof of the stupid nat thing, just figure out why $ik+jl+mq+np-(mp+nq+il+kj)$ is in the ideal of $\mathbb{Z}[i,j,k,l,m,n,p,q]$ generated by the relations (i.e. write it explicitly as a linear combination), then tidy up to get rid of all `neg`

s, prove it by `ring`

and then you're just a rewrite away.

Last updated: May 06 2021 at 17:38 UTC