## Stream: new members

#### Jz Pan (Dec 23 2020 at 12:03):

I'd like to prove the following result (this is the discriminant of an elliptic curve with j-invariant equal to j):

example (j : ℚ) (h0 : j ≠ 0) (h1728 : j-1728 ≠ 0) :
((-36) / (j - 1728)) ^ 2 - (-1) / (j - 1728) - 8 * (2 * ((-36) / (j - 1728))) ^ 3 - 27 * (4 * ((-1) / (j - 1728))) ^ 2 + 9 * (2 * ((-36) / (j - 1728))) * (4 * ((-1) / (j - 1728))) ≠ 0 :=
begin
calc ((-36) / (j - 1728)) ^ 2 - (-1) / (j - 1728) - 8 * (2 * ((-36) / (j - 1728))) ^ 3 - 27 * (4 * ((-1) / (j - 1728))) ^ 2 + 9 * (2 * ((-36) / (j - 1728))) * (4 * ((-1) / (j - 1728)))
= j^2 / (j-1728)^3 : by {
field_simp [h1728],
sorry,
}
... ≠ 0 : by {
field_simp [h1728, h0],
},
end


but the first field_simp seems not work. Any suggestions?

#### Johan Commelin (Dec 23 2020 at 12:23):

the goal is changing before and after the first field_simp, right?

#### Eric Wieser (Dec 23 2020 at 12:25):

Yes, field_simp seems to be doing it's job

#### Eric Wieser (Dec 23 2020 at 12:25):

You can close that sorry with ring_exp, ring

#### Sebastien Gouezel (Dec 23 2020 at 12:25):

ring is enough.

#### Sebastien Gouezel (Dec 23 2020 at 12:26):

Is that a ring_exp bug that it doesn't close this goal, by the way?

#### Johan Commelin (Dec 23 2020 at 12:26):

Eric Wieser said:

Yes, field_simp seems to be doing it's job

Well, it didn't clear all denominators.

#### Johan Commelin (Dec 23 2020 at 12:26):

field_simp [pow_succ, h1728] does clear all denoms.

#### Sebastien Gouezel (Dec 23 2020 at 12:27):

Here, it does close all denominators.

#### Kevin Buzzard (Dec 23 2020 at 12:28):

You were fiddling with attributes the other day though

#### Johan Commelin (Dec 23 2020 at 12:29):

ooh, maybe I'm on a mathlib that's too old

#### Jz Pan (Dec 23 2020 at 12:39):

Thanks, I confirm that

  = j^2 / (j-1728)^3 : by {
field_simp [pow_succ, h1728],
ring,
}


works. Maybe I'm using an old version of mathlib, who knows. Anyway I already fixed it by using another elliptic curve whose a1 a2 a3 a4 a6 have no denominators (using a linear change of variable to eliminate all its denominators) :smile:

#### Kevin Buzzard (Dec 23 2020 at 13:29):

I tried to prove the group law was associative for the general a1 a2...a6 form and lean got bogged down in the algebra. I am running a student project on elliptic curves next term and I was tempted to just stick to x^3+Ax+B.

#### Jz Pan (Dec 24 2020 at 05:58):

Interesting. I heard that somebody already implemented the group law for general Weierstrass form.

#### Johan Commelin (Dec 24 2020 at 06:00):

I think that was Kevin, together with John Cremona. But I'm not sure if they finished it in the end. Kevin's comment above sounds like they didn't...

#### Kevin Buzzard (Dec 24 2020 at 09:58):

Oh I'm sure this has been done in other provers. Cremona and I have some work we were doing for fun at LFTCM

#### Jz Pan (Dec 25 2020 at 08:19):

Oops, when I upgrade the mathlib my old file breaks, which complains with 'unknown identifier field_simp'. The last version I used is around 12-02.

#### Ruben Van de Velde (Dec 25 2020 at 08:45):

Try adding import tactic.field_simp?

#### Jz Pan (Dec 25 2020 at 09:12):

And then it doesn't solve the goal anymore :neutral:

#### Eric Wieser (Dec 25 2020 at 09:12):

How close does it get?

#### Jz Pan (Dec 25 2020 at 09:17):

How close does it get?

I forgot; I have already revert the mathlib version :|

#### Johan Commelin (Dec 25 2020 at 09:45):

field_simp became more powerful... so if it stopped closing a goal, we would be interested to know what it looks like...

#### Jz Pan (Dec 26 2020 at 07:21):

You can go to https://gitee.com/acmepjz/my-lean-test/tree/master/tests/gtm106 for my test codes. Current I'm using mathlib version 1f1ba587f272d203a40801c6b21af453f7de6ee3 2020-11-29 and all of my code works.

Last updated: May 08 2021 at 18:17 UTC