## 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 negs, prove it by ring and then you're just a rewrite away.

Last updated: May 06 2021 at 17:38 UTC