# Zulip Chat Archive

## Stream: general

### Topic: 100 theorems

#### Floris van Doorn (May 29 2019 at 21:24):

I'm updating the 100 theorems for Lean: https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md

for Freek's 100 theorem project: http://www.cs.ru.nl/~freek/100/

Who should I cite as the author for De Moivre's Theorem?

- Abhimanyu Pallavi Sudhir, who did the actual theorem (link)
- Chris Hughes, who did (or at least committed) all the work, so that the theorem could be proven in a few lines
- or mathlib

#### Floris van Doorn (May 29 2019 at 21:30):

I'm going through Mario's list. I don't think we have Brouwer's fixed point theorem. I can only find the Banach fixed point theorem: https://github.com/leanprover-community/mathlib/blob/f25340175631cdc85ad768a262433f968d0d6450/src/topology/metric_space/lipschitz.lean#L110

#### Floris van Doorn (May 29 2019 at 21:46):

Do we have Bezout's theorem in mathlib? The closest I can find is https://github.com/leanprover-community/mathlib/blob/78f1949719676db358ea5e68e211a73e2ce95e7b/src/data/int/modeq.lean#L107

#### Neil Strickland (May 29 2019 at 21:56):

I don't think we can do the Brouwer fixed point theorem without knowing either \pi_n or H_n of the n-sphere. (Either one would do, but H_n would be tidier.) It looks like @Reid Barton has defined \pi_n but we don't have any calculations and we don't have H_n.

#### Floris van Doorn (May 29 2019 at 21:57):

We had the number of combinations in Lean 2: https://github.com/leanprover/lean2/blob/227fcad22ab2bc27bb7471be7911075d101ba3f9/library/theories/combinatorics/choose.lean#L208

I don't think it's in Lean 3 yet. Someone port this! :)

#### Neil Strickland (May 29 2019 at 22:06):

That's `card_powerset_len`

at https://github.com/leanprover-community/mathlib/blob/00aaf05a00b928ea9ac09721d87ae5d2ca1ae5a1/src/data/finset.lean#L1300

#### Floris van Doorn (May 29 2019 at 22:12):

Thanks!

#### Floris van Doorn (May 29 2019 at 22:12):

Ah, when searching for the Euclidean Algorithm, I found Bezout's theorem:

https://github.com/leanprover-community/mathlib/blob/4845b663c182704738868db5861ffb4c6056be23/src/algebra/euclidean_domain.lean#L233

#### Kevin Buzzard (May 29 2019 at 22:17):

72. Sylow’s Theorem

What even is Sylow's Theorem? Chris proved all three Sylow Theorems as part of his 1st year project last year: https://github.com/ChrisHughes24/Sylow . The things I was told were Sylow's theorems are all pretty near the bottom of the file.

#### Floris van Doorn (May 29 2019 at 22:19):

What should I cite as the Euclidean Algorithm? Maybe just the definition of `gcd`

?

def gcd : α → α → α | a := λ b, if a0 : a = 0 then b else have h:_ := mod_lt b a0, gcd (b%a) a using_well_founded {dec_tac := tactic.assumption, rel_tac := λ _ _, `[exact ⟨_, r_well_founded α⟩]}

#### Floris van Doorn (May 29 2019 at 22:22):

@Kevin Buzzard I think these three theorems: https://en.wikipedia.org/wiki/Sylow_theorems

I saw the first one at the bottom of the `sylow.lean`

file in mathlib, and therefore assumed that the other 2 were not yet proven, but I'll dig a little deeper.

#### Neil Strickland (May 29 2019 at 22:22):

The Isabelle version proves only the existence of Sylow p-subgroups, which is what we have in mathlib. HOL Light, Metamath, Coq and Mizar all have the other theorems: all Sylow subgroups are conjugate, and their number is congruent to one mod p and divides the order of the group. These also appear in Chris's repository, and should certainly move into mathlib at some point.

#### Kevin Buzzard (May 29 2019 at 22:24):

I don't know what made it into mathlib; my post linked to the repo Chris wrote for his project. I'm assuming we can link to non-mathlib stuff?

#### Floris van Doorn (May 29 2019 at 22:25):

Of course! I'll link to that repository.

#### Chris Hughes (May 29 2019 at 22:28):

I should PR the other two theorems at some point. Haven't done it yet.

#### Floris van Doorn (May 29 2019 at 22:30):

Did you formalize the last part of Theorem 3?

`np = |G : NG(P)|`

, where P is any Sylow p-subgroup of G and NG denotes the normalizer.

#### Floris van Doorn (May 29 2019 at 22:34):

Should I cite Leo de Moura author of The Principle of Mathematical Induction in Lean? :P

#### Floris van Doorn (May 29 2019 at 22:53):

Have we proven that `int`

is a `unique_factorization_domain`

?

#### Chris Hughes (May 29 2019 at 22:59):

We have proven that int is a UFD. This is probably multiple authors, because it goes via general results about Euclidean domains and PIDs. But mainly Johannes. It's there for nat as well, and that was Mario.

#### Neil Strickland (May 29 2019 at 23:03):

In `algebra.euclidean_domain`

we have `int.euclidean_domain`

. In `ring_theory.principal_ideal_domain`

we have ` euclidean_domain.to_principal_ideal_domain`

and `principal_ideal_domain.to_unique_factorization_domain`

.

#### Floris van Doorn (May 29 2019 at 23:04):

Ah, thanks!

#### Floris van Doorn (May 29 2019 at 23:05):

I'll use `mathlib`

as the author.

#### Chris Hughes (May 29 2019 at 23:05):

I don't think I formalised that last part of theorem three. I don't understand your statement.

#### Floris van Doorn (May 29 2019 at 23:06):

Ok. It's the last bullet point of Theorem 3 from Wikipedia: https://en.wikipedia.org/wiki/Sylow_theorems

#### Neil Strickland (May 29 2019 at 23:09):

But `principal_ideal_domain.to_unique_factorization_domain`

is not an instance, so `by apply_instance : unique_factorization_domain ℤ`

fails. I'm not sure why that is. It might be related to the fact that `principal_ideal_domain.to_unique_factorization_domain`

is marked as `noncomputable`

.

#### Chris Hughes (May 29 2019 at 23:11):

It is because of that fact.

#### Neil Strickland (May 29 2019 at 23:14):

That bullet point is the `have`

at line 935 of https://github.com/ChrisHughes24/Sylow/blob/master/src/sylow.lean, but it is not stated as a separate theorem.

#### Floris van Doorn (May 29 2019 at 23:17):

Ah, ok. Then I'll just write that.

#### Rob Lewis (May 29 2019 at 23:31):

I can claim an earlier proof of the IVT, although I'm not sure we want to draw anyone's attention to the days before simp and style conventions! https://github.com/leanprover/lean2/blob/master/library/theories/analysis/ivt.lean

#### Floris van Doorn (May 29 2019 at 23:32):

I updated the markdown file. We have formalized 23/100 results (that I could find).

#### Floris van Doorn (May 29 2019 at 23:32):

https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md

#### Floris van Doorn (May 29 2019 at 23:36):

The ones on Mario's list that I couldn't find:

- 78 (cauchy-schwarz)
- 94 (law of cosines)

#### Floris van Doorn (May 29 2019 at 23:41):

In cases that there is not a clear single author, I now liberally used `mathlib`

as an author. If anyone is unhappy with that, feel free to change it.

#### Chris Hughes (May 29 2019 at 23:46):

I don't think I should be the author of Bezout's theorem. I more or less copied that proof exactly from the nat version.

#### Floris van Doorn (May 29 2019 at 23:48):

Ok, I'll change it to mathlib.

I used Github's history to figure out authorship. This is of course a flawed method. Please check if there are attributions which are clearly wrong.

#### Floris van Doorn (May 30 2019 at 01:31):

I emailed Freek to point him to the markdown file (Lean now looks so sad with a score of 1 on his page).

#### Neil Strickland (May 30 2019 at 06:59):

At http://bim.shef.ac.uk/lean/hundred_theorems.html I put a crude analysis of what would be needed for the remaining theorems.

#### Mario Carneiro (May 30 2019 at 07:40):

I think both law of cosines and cauchy schwarz are "in the air" at this point, i.e. someone just has to actually write down and prove the statement

#### Mario Carneiro (May 30 2019 at 07:41):

for law of cosines, I'm not quite sure how to do it in a general vector space without it being tautological

#### Kenny Lau (May 30 2019 at 07:42):

I thought 6. Godel's Incompleteness Theorem was already done?

#### Mario Carneiro (May 30 2019 at 07:48):

certainly not. I think isabelle has the only known proof

#### Mario Carneiro (May 30 2019 at 07:48):

oh, Freek says there are also others

#### Mario Carneiro (May 30 2019 at 07:49):

but it's one of the "hard problems" on the list

#### Mario Carneiro (May 30 2019 at 07:49):

you have to build proof theory first

#### Kenny Lau (May 30 2019 at 07:51):

I thought someone proved it in the conference we went to

#### Kenny Lau (May 30 2019 at 07:52):

I remember the independence of continuum hypothesis having been proved

#### Kenny Lau (May 30 2019 at 07:52):

so there is definitely a proof theory

#### Mario Carneiro (May 30 2019 at 07:53):

That's true, Floris and Jesse are soon to be the first to do the independence of the continuum hypothesis, and they had to build a proof theory for that

#### Mario Carneiro (May 30 2019 at 07:53):

but they didn't do anything with arithmetization (although I did, for computability stuff)

#### Mario Carneiro (May 30 2019 at 07:55):

you still have to do quite a lot of work in the embedded proof theory (basically PA), and we're slowly learning how to do that without tearing our hair out

#### Scott Morrison (May 30 2019 at 07:55):

@Martin Skilleter has the Cauchy-Schwarz inequality.

#### Patrick Massot (May 30 2019 at 08:42):

https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md#86-lebesgue-measure-and-integration is misleading. This is not Lebesgue integral.

#### Mario Carneiro (May 30 2019 at 08:47):

I don't think it is. It's less than we want from our integration library, but it's definitely the lebesgue measure and the integral on that measure

#### Mario Carneiro (May 30 2019 at 08:48):

if anything, the problem with this challenge in general is that there's no clear theorem or definition to point to

#### Mario Carneiro (May 30 2019 at 08:48):

it's really a statement about a whole construction

#### Keeley Hoek (May 30 2019 at 08:48):

Perhaps a link to the "main" file?

#### David Michael Roberts (May 30 2019 at 10:27):

That's true, Floris and Jesse are soon to be the first to do the independence of the continuum hypothesis, and they had to build a proof theory for that

So where is the constructible universe up to (or are they using the hierarchy that uses HOD instead of L?)

#### Mario Carneiro (May 30 2019 at 10:32):

I don't think they are planning on doing L, actually. Jesse says there is a way to do it with forcing, which will be nice if true since they already had to build all that for the first part (proving that CH is unprovable)

#### David Michael Roberts (May 30 2019 at 11:56):

Oh, I see, collapsing P(N) to aleph_1. Nice.

#### David Michael Roberts (May 30 2019 at 11:58):

"Just" construct the correct boolean algebra and turn the handle to get new model of ZFC, and then show CH is true therein. :-)

#### Floris van Doorn (May 30 2019 at 16:33):

@Martin Skilleter If you give a link to your formalization of the Cauchy-Schwarz inequality, I will link to it.

#### Floris van Doorn (May 30 2019 at 16:36):

@Patrick Massot What is missing from the definition of the Lebesgue integral? I'm happy to remove if something is missing. I agree with Mario that the challenge is stupid because it asks for a definition, not the proof of a theorem.

#### Mario Carneiro (May 30 2019 at 16:37):

One reasonable argument you can levy against our integral is that it doesn't support functions R -> R

#### Mario Carneiro (May 30 2019 at 16:38):

to which we say "Bochner integral is coming" and by then we've already shot right past the conventional definition

#### Floris van Doorn (May 30 2019 at 16:39):

@Neil Strickland Nice list! Doing the `Arithmetic Mean/Geometric Mean`

should be a small project if done directly (there is a pretty easy induction argument, which shows that if the inequality holds for `n`

then it holds for `2n`

and `n-1`

), but what we probably want is to show that the Power mean is an increasing function.

#### Floris van Doorn (May 30 2019 at 16:42):

@Mario Carneiro Oh, that's fair. Do you think that is big enough of an omission to remove it from the list?

#### Mario Carneiro (May 30 2019 at 16:43):

I don't, as I said to Patrick. I think that we've done all the important stuff that pertains to lebesgue integral already. In the future when we have Bochner integral and are asked to identify where is the Lebesgue integral, we will still point to the ennreal definition

#### Reid Barton (Jun 01 2019 at 06:43):

I have (23) Formula for Pythagorean Triples on my old laptop. It was part of my first real Lean project.

I can try updating it to modern mathlib when I get home.

#### Reid Barton (Jun 01 2019 at 07:07):

A year later, I'm still not sure what the mathlib-approved way to talk about even and odd numbers is.

#### Alex J. Best (Jun 11 2019 at 09:19):

I just finished having a go at one of these, every prime congruent to 1 mod 4 is a sum of two squares (@Chris Hughes has already done it, but my version is quite... different). I tried to formalise Don Zagier's (in)famous one-sentence proof https://people.mpim-bonn.mpg.de/zagier/files/doi/10.2307/2323918/fulltext.pdf it turned out to be a few more than 1 sentence of course, but I stuck pretty much exactly to the intended argument.

I'd appreciate any comments people have (especially on how to break it up into separate lemmas, or reduce its size, in the course of the proof it has turned into one giant, semi-impossible-to-compile monolith so. I tried but sort of gave up on shrinking it now). I'm pretty sure it compiles, but my computer times out if I try and do it all in one go.

This was the first big project I've tried so fair to say, I learned a lot!

https://gist.github.com/alexjbest/1fcc06a67f4d56275f99c44037bb1b6d

#### Johan Commelin (Jun 11 2019 at 09:26):

Wow, that's almost 500 lines of proof!

#### Kevin Buzzard (Jun 11 2019 at 09:58):

The timeout might not be because of your computer -- it might be a more serious problem.

#### Kevin Buzzard (Jun 11 2019 at 09:59):

oh wait -- I can get it to compile from the command line. so I think it's OK! Well done!

#### Alex J. Best (Jun 11 2019 at 09:59):

Oh its definitely a serious problem, I didn't mean to imply that it wasn't! But probably there is a solution I'm not aware of, every time I tried to break it up into lemmas it all broke as everything depends on p is all.

#### Kevin Buzzard (Jun 11 2019 at 10:00):

wait, I spoke too soon :-/

#### Kevin Buzzard (Jun 11 2019 at 10:01):

prime.lean:614:0: error: invalid assertv tactic, value has type ↥fixp_j but is expected to have type fixp_j state: p : ℕ, pprime : nat.prime p, p1mod4 : p % 4 = 1, property : ℤ3 → Prop := prod.rec (λ (fst : ℤ), prod.rec (λ (snd_fst snd_snd : ℤ), id_rhs Prop (fst ^ 2 + 4 * snd_fst * snd_snd = ↑p ∧ fst > 0 ∧ snd_fst > 0 ∧ snd_snd > 0))), S : Type := subtype property, big_set : Type := fin p × fin p × fin p, _inst : fintype big_set, random_func : S → big_set := λ (a : S), subtype.cases_on a (λ (a_val : ℤ3) (P : property a_val), prod.cases_on a_val (λ (X : ℤ) (a_val_snd : ℤ × ℤ) (P : property (X, a_val_snd)), prod.cases_on a_val_snd (λ (Y Z : ℤ) (P : property (X, Y, Z)), (⟨int.nat_abs X, _⟩, ⟨int.nat_abs Y, _⟩, ⟨int.nat_abs Z, _⟩)) P) P), random_inj : function.injective random_func, _inst_1 : fintype S, mainn : fintype.card S ≡ 1 [MOD 2], j : S → S := λ (a : S), subtype.cases_on a (λ (a_val : ℤ3) (P : property a_val), prod.cases_on a_val (λ (X : ℤ) (a_val_snd : ℤ × ℤ) (P : property (X, a_val_snd)), prod.cases_on a_val_snd (λ (Y Z : ℤ) (P : property (X, Y, Z)), ⟨(X, Z, Y), _⟩) P) P), j_invo : funcpow j 2 = id, _inst_2 : mul_action (fin 2) S := finorder_end_cyclic_action j_invo, fixp_j : set S := fixed_points (fin 2) S, finj : fintype ↥fixp_j, exists_fixed_j : nonempty ↥fixp_j ⊢ ∃ (a b : ℤ), a ^ 2 + b ^ 2 = ↑p

#### Kevin Buzzard (Jun 11 2019 at 10:01):

Oh its definitely a serious problem, I didn't mean to imply that it wasn't! But probably there is a solution I'm not aware of, every time I tried to break it up into lemmas it all broke as everything depends on p is all.

This can surely be solved.

#### Alex J. Best (Jun 11 2019 at 10:07):

prime.lean:614:0: error: invalid assertv tactic, value has type ↥fixp_j but is expected to have type fixp_j state: p : ℕ, pprime : nat.prime p, p1mod4 : p % 4 = 1, property : ℤ3 → Prop := prod.rec (λ (fst : ℤ), prod.rec (λ (snd_fst snd_snd : ℤ), id_rhs Prop (fst ^ 2 + 4 * snd_fst * snd_snd = ↑p ∧ fst > 0 ∧ snd_fst > 0 ∧ snd_snd > 0))), S : Type := subtype property, big_set : Type := fin p × fin p × fin p, _inst : fintype big_set, random_func : S → big_set := λ (a : S), subtype.cases_on a (λ (a_val : ℤ3) (P : property a_val), prod.cases_on a_val (λ (X : ℤ) (a_val_snd : ℤ × ℤ) (P : property (X, a_val_snd)), prod.cases_on a_val_snd (λ (Y Z : ℤ) (P : property (X, Y, Z)), (⟨int.nat_abs X, _⟩, ⟨int.nat_abs Y, _⟩, ⟨int.nat_abs Z, _⟩)) P) P), random_inj : function.injective random_func, _inst_1 : fintype S, mainn : fintype.card S ≡ 1 [MOD 2], j : S → S := λ (a : S), subtype.cases_on a (λ (a_val : ℤ3) (P : property a_val), prod.cases_on a_val (λ (X : ℤ) (a_val_snd : ℤ × ℤ) (P : property (X, a_val_snd)), prod.cases_on a_val_snd (λ (Y Z : ℤ) (P : property (X, Y, Z)), ⟨(X, Z, Y), _⟩) P) P), j_invo : funcpow j 2 = id, _inst_2 : mul_action (fin 2) S := finorder_end_cyclic_action j_invo, fixp_j : set S := fixed_points (fin 2) S, finj : fintype ↥fixp_j, exists_fixed_j : nonempty ↥fixp_j ⊢ ∃ (a b : ℤ), a ^ 2 + b ^ 2 = ↑p

oh oops I broke it trying to improve readability line 614 just remove the type and it should go, I updated the gist. Thanks!

#### Kevin Buzzard (Jun 11 2019 at 10:09):

If in VS Code you do File -> Preferences -> Settings (or ctrl-,) then search for lean then scroll down until you find "Lean time limit" and change the value from 100000 to 500000 then it will remove the deterministic timeout.

#### Kevin Buzzard (Jun 11 2019 at 10:12):

You could define functions `S p`

and `bigset p`

etc. I'm still getting timeouts :-( There is maybe some type error somewhere, or the elaborator is going off doing something it shouldn't be doing, or something.

#### Kevin Buzzard (Jun 11 2019 at 10:14):

You must have had the patience of a saint to use Lean like this -- waiting forever for things to compile drives me nuts.

#### Alex J. Best (Jun 11 2019 at 10:25):

Yeah I ended up sorrying and commenting a lot, and having a separate scratch section for running library search and building snippets of proof up... having to do "real work" while lean is compiling wasn't the worst thing ever though

#### Kevin Buzzard (Jun 11 2019 at 11:14):

There seems to be some sort of a problem around line 569 but it's particularly obscure.

Inserting `sorry, end, sorry, end #exit`

just after `rw one_fixed_i at mainn,`

gets the proof compiling. However inserting `end, sorry, end #exit`

instead, just after the next line `exact mainn`

causes a deterministic time-out, even if the time-out variable is set to super-high (900000). We had this problem in the perfectoid project and it turned out to be a delicate issue with unification which was very hard to debug.

#### Kevin Buzzard (Jun 11 2019 at 11:14):

In short, our code was crummy in a way we had not really understood because the issue was not mathematical.

#### Kevin Buzzard (Jun 11 2019 at 11:16):

I would honestly recommend breaking up the proof into much smaller chunks so it's easier to find out what's going on. It's very frustrating to work with it as things stand.

#### Kevin Buzzard (Jun 11 2019 at 11:18):

Other comments: indent 2 spaces not 4, and indent after the initial `begin`

so that the entire proof is two spaces in (at least).

#### Alex J. Best (Jun 11 2019 at 12:10):

Thanks, I filled in a couple more underscores there, maybe it will help a little. I think I fixed a more serious problem which was messing my lean up, lots of `dsimp at *`

's later on in the proof were screwing with earlier results it seems. Yet more reasons not to make one huge proof I guess.

#### Alex J. Best (Jun 11 2019 at 22:40):

I would honestly recommend breaking up the proof into much smaller chunks so it's easier to find out what's going on. It's very frustrating to work with it as things stand.

Okay I did that and it seems to work really quite well now, thanks for the recommendation

https://gist.github.com/alexjbest/1fcc06a67f4d56275f99c44037bb1b6d

I have one concrete question now, which should be easier to answer now that it compiles in seconds not minutes...

In my lemma i_invo if I delete the line `unfold funcpow`

and let the `dsimp`

line below unfold it looks like the proof works unchanged in the goal view, but I get a weird error message I don't understand, `type mismatch at application id`

.. and then a lot of output. Whats going on here?

#### Kevin Buzzard (Jun 11 2019 at 22:48):

Your proof compiles fine for me now! Congratulations on proving what is quite a tricky theorem!

#### Kevin Buzzard (Jun 11 2019 at 22:50):

If I comment out `unfold funcpow`

on line 348 the proof still compiles fine.

#### Floris van Doorn (Jul 01 2019 at 11:38):

What happened to the `100-thms`

branch? It doesn't exist anymore: https://github.com/leanprover-community/mathlib/tree/100-thms

#### Floris van Doorn (Jul 01 2019 at 12:59):

I pushed the branch I had locally. I don't know if we lost any commits. Is there an (automatic) cleanup of branches in mathlib?

#### Johan Commelin (Jul 01 2019 at 20:48):

I would hope there is not... I didn't backup this branch :-(

#### Floris van Doorn (Aug 06 2019 at 21:40):

I added 3. The Denumerability of the Rational Numbers and 22. The Non-Denumerability of the Continuum. Have any others been proven recently?

I'll message Freek soon to update his list.

#### Kevin Buzzard (Aug 06 2019 at 22:02):

Not all primes are the sum of two squares (number 20 title)

#### Floris van Doorn (Aug 06 2019 at 23:06):

thanks, I fixed the title.

#### Johan Commelin (Sep 01 2020 at 08:14):

@Freek Wiedijk We have 5 new items for your list:

https://github.com/leanprover-community/leanprover-community.github.io/commits/newsite/data/100.yaml

#### Rob Lewis (Sep 01 2020 at 08:16):

Hmm, but https://leanprover-community.github.io/100.html doesn't seem to have updated yet

#### Floris van Doorn (Jan 08 2021 at 19:57):

Freek just updated http://www.cs.ru.nl/~freek/100/

#### Kevin Buzzard (Jan 08 2021 at 20:35):

We're over half way there! And area of a circle is on the horizon...

#### Floris van Doorn (Jan 08 2021 at 23:33):

Yeah, there are many results that are within reach with the current state of the library. We also have open PRs for 30 (#5574) and 45 (#4259).

#### Ruben Van de Velde (Jan 09 2021 at 09:01):

Do we not have the cubic formula (37) yet? Any reason why it'd be hard?

#### Kenny Lau (Jan 09 2021 at 09:02):

I don't think it should be hard.

#### Johan Commelin (Jan 09 2021 at 09:07):

It would be good to make it general (as in, not just over the reals).

#### Kevin Buzzard (Jan 09 2021 at 09:46):

Would it? Doing it over the complexes would be easiet because all square and cube roots exist. In small characteristic there are problems (formula isn't true). Over a general field of char 0 (say) one has to decide what the statement is. There are times when the auxiliary square roots don't exist in the field and yet the cubic has a root anyway. I guess one could dodge all this by saying "the roots are this in the algebraic closure" but then you may as well be working over the complexes anyway

#### Chris Hughes (Jan 09 2021 at 11:44):

You just want the a variable and a hypothesis that they are a cube root.

#### Ruben Van de Velde (Jan 09 2021 at 11:46):

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/quadratic_discriminant.lean does something like that, yeah. I think the problem is with the intermediate square roots, though

#### Johan Commelin (Jan 09 2021 at 13:48):

@Kevin Buzzard but if at some point we want to apply this, then it probably won't be over `complex`

...

Last updated: May 15 2021 at 22:14 UTC