# Zulip Chat Archive

## Stream: new members

### Topic: complex.I is algebraic !

#### Nicolás Ojeda Bär (Oct 12 2019 at 21:43):

Hurrah! I installed Lean yesterday evening, and after "just" a day and a half, I managed to prove my first result, namely that `i`

is algebraic. Surely experts should be able to condense my proof to just a few words; please share any advice you may have (tactics, style, etc.). Thanks!

import ring_theory.algebra open polynomial universes u v variables (k : Type u) (R : Type v) variables [field k] [comm_ring R] [algebra k R] def is_algebraic (x : R) := ∃ p, monic p ∧ aeval k R x p = 0 lemma degree_one_le_1 : degree (1 : polynomial k) ≤ 1 := begin norm_num, exact (with_bot.coe_le_coe.2 (by simp)) end example : is_algebraic ℝ ℂ complex.I := begin unfold is_algebraic, use (X^2 + 1), split, { -- prove monic (X^2 + 1) exact (monic_X_pow_add (degree_one_le_1 _)) }, { -- prove that I^2 + 1 = 0 rewrite aeval_def, rewrite (pow_two X), simp } end

#### Reid Barton (Oct 12 2019 at 21:58):

My expert tip: `rw`

is shorter than `rewrite`

#### Alex J. Best (Oct 12 2019 at 22:43):

I'm not an expert, but here's where I'd take it too if I found the same proof,

import ring_theory.algebra import tactic.library_search -- how I "remembered" the name of degree_one just ask library_search open polynomial complex -- so I can write I instead of complex.I universes u v variables (k : Type u) {R : Type v} -- I changed R to be implicit as we want it to be in is_algebraic, there is no need to specify R twice, as its already just whatever ring x is a term of and x is in the definition variables [field k] [comm_ring R] [algebra k R] def is_algebraic (x : R) := ∃ p, monic p ∧ aeval k R x p = 0 example : is_algebraic ℝ I := -- making R implicit above lets me remove \C here, opening complex lets me just write I begin -- removed the unfold as it's not needed (except to find the proof in the first place) use (X^2 + 1), split, { -- prove monic (X^2 + 1) exact (monic_X_pow_add (by rw degree_one; exact dec_trivial)) -- there is a lemma saying degree of 1 is 0 already, so use it and then 0 \le \u 1 is boring so hit it with dec_trivial, probably there is a lemma for this but dec_trivial is good. }, { -- prove that I^2 + 1 = 0 simp [aeval_def, pow_two], -- bit of golfing, personal preference and not necessary, but is more like the human "simplify everything using the definition and that x^2=x" } end

#### Alex J. Best (Oct 12 2019 at 22:45):

And yeah probably someone here can get a one-line proof of this ;) but this seems a good balance to me

#### Alex J. Best (Oct 12 2019 at 22:53):

oops, confused myself and forgot the earlier conversation, integral = algebraic over a field!

#### Floris van Doorn (Oct 13 2019 at 05:53):

Here is my try. I didn't change Alex's proof, but I did change the statement. If we want to prove that `i`

is algebraic, we really want to prove that it's algebraic over `Q`

. I had to add some instances for Lean to recognize that `C`

is an algebra over `Q`

. These should be added to mathlib. Also, Alex's proof was robust enough to work without changes!

import ring_theory.algebra open polynomial complex instance rat.cast.is_ring_hom {α} [division_ring α] [char_zero α] : is_ring_hom (rat.cast : ℚ → α) := ⟨rat.cast_one, rat.cast_mul, rat.cast_add⟩ instance algebra_rat {α} [field α] [char_zero α] : algebra ℚ α := algebra.of_ring_hom rat.cast (by apply_instance) universes u v variables (k : Type u) {R : Type v} variables [field k] [comm_ring R] [algebra k R] def is_algebraic (x : R) := ∃ p, monic p ∧ aeval k R x p = 0 example : is_algebraic ℚ I := begin use (X^2 + 1), split, { exact (monic_X_pow_add (by rw degree_one; exact dec_trivial)) }, { simp [aeval_def, pow_two] } end

#### Alex J. Best (Oct 13 2019 at 06:05):

Nice, definitely these should end up in mathlib. I also worked on getting exactly the same cast going to prove that X^2 + 1 was monic actually, I was hoping that dec_trivial would prove that monic polynomials over Q were in fact monic, and then the proof for R could involve `convert (monic_map (rat.cast : ℚ → ℝ)) (dec_trivial : (monic : polynomial ℚ → Prop)(X^2 + 1)),`

I was hoping that this would be even more robust, and you could show that every polynomial which is "obviously" monic over Q was monic without work this way, rather than worrying about special lemmas on the form of the polynomial. But I couldn't make a decidable instance for polynomial.monic that was computable. I guess this is due to some lines in the polynomial files like noncomputable theory and prop_decidable instances, but I think it would be nice if this could work, is there a reason not to allow this sort of thing? Or am I missing an existing way to do this?

#### Keeley Hoek (Oct 13 2019 at 06:39):

There is an instance for decidability of monic-ness, `monic.decidable`

, but it doesn't work at the moment in this case

instance dinst : decidable (@monic ℚ _ (X^2 + 1)) := by apply_instance

because of picking up classical stuff in the polynomial development

#### Nicolás Ojeda Bär (Oct 13 2019 at 08:48):

1) Just to confirm my understanding, what is the difference between `rw aeval_def`

and `simp [aeval_def]`

?

2) How does it work in `simp [pow_two]`

where the argument (`X`

) is not passed (not even with a wildcard `_`

)?

#### Patrick Massot (Oct 13 2019 at 08:49):

Did you read https://leanprover.github.io/theorem_proving_in_lean/tactics.html#rewriting and the next section?

#### Nicolás Ojeda Bär (Oct 13 2019 at 08:51):

No, not yet, I will do it now. Thanks for the hint!

#### Kevin Buzzard (Oct 13 2019 at 08:51):

`rw h`

means "find the left hand side of `h`

in the goal and replace it with the right hand side. `simp [h]`

means "you can use `h `

and also every single lemma tagged `[simp]`

in core Lean and also every module you've imported, all applied according to some clever heuristics which you don't need to know about"

Last updated: May 13 2021 at 06:15 UTC