Zulip Chat Archive

Stream: maths

Topic: integer multiplication well-defined


view this post on Zulip 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 N2/\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.

view this post on Zulip Kenny Lau (Jan 06 2020 at 04:53):

maybe don't use equivalence relation

view this post on Zulip Kenny Lau (Jan 06 2020 at 04:54):

use quot and r (i,j) (i+1,j+1)

view this post on Zulip Kevin Buzzard (Jan 06 2020 at 04:55):

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

view this post on Zulip 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)ik+jl+mq+np-(mp+nq+il+kj) is in the ideal of Z[i,j,k,l,m,n,p,q]\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