Stream: new members

Topic: How to multiply an integer times a real

Lars Ericson (Jan 05 2021 at 23:42):

The first check works and the second throws an error:

import data.real.basic
import analysis.special_functions.pow

variable a : ℤ

#check ((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) -- OK

#check a*((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) -- error


The error is

foo1.lean:8:16
type mismatch at application
pow 9
term
9
has type
ℝ
but is expected to have type
ℤ
foo1.lean:8:16
failed to synthesize type class instance for
a : ℤ
⊢ has_pow ℤ ℝ


I'm trying to figure out how to state this theorem:

import data.real.basic
import analysis.special_functions.pow

theorem ex6e_mul_closed (a b c d : ℤ):
(a + b * ((9:ℝ) ^ ((1:ℝ)/(4:ℝ)))) * (c + d * ((9:ℝ) ^ ((1:ℝ)/(4:ℝ))))=
(a * c + b * d * 3) + (a*d + b * c) * ((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) :=
sorry


Kevin Buzzard (Jan 05 2021 at 23:50):

Lean reads from left to right. Read a*((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) from left to right. First we see a. This is an integer. Then we see *. That is multiplication, which takes two elements of type X and returns an element of type X. Then we solve for X, and it's easy to solve -- a is an integer, so X must be the integers. Then we read on and see real numbers instead of integers. Then we get confused and produce an error.

Kevin Buzzard (Jan 05 2021 at 23:51):

The fix is to not let Lean solve for X incorrectly, by not letting it see the integer a, e.g. by writing (a : ℝ) instead of a. Then it will set X = reals and then you should hopefully be fine.

Lars Ericson (Jan 06 2021 at 00:51):

The problem is that I have to have a be an integer for this particular theorem. That's why I said variable a : ℤ. I am trying to prove that expressions of form a + b * 9^(1/4) are closed under multiplication, where a and b are integers and 9^(1/4) is a particular irrational number. Writing a : ℝ won't get me there.

Bryan Gin-ge Chen (Jan 06 2021 at 00:54):

I think Kevin's suggestion is not to replace the variable statement, but to add the type coercion to the expression you're interested in:

import data.real.basic
import analysis.special_functions.pow

variable a : ℤ

#check ((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) -- OK

#check (a : ℝ)*((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) -- also OK


Lars Ericson (Jan 06 2021 at 01:05):

Thanks @Kevin Buzzard and @Bryan Gin-ge Chen. The following is a bit more awkward but it better represents what I am trying to prove, and doesn't raise an error, I guess because the subring tells Lean something that makes it find a has_pow for this case:

import data.real.basic
import analysis.special_functions.pow

theorem ex6e_mul_closed : ∃ s : subring ℝ,
∀ x y z: ℝ,
x ∈ s →
y ∈ s →
z ∈ s →
∀ a b c d: ℤ,
x = a + b * ((9:ℝ) ^ (1/4:ℝ)) →
y = c + d * ((9:ℝ) ^ (1/4:ℝ)) →
z = x * y →
z = (a * c + b * d * 3) + (a * d + b * c) * (9:ℝ) ^ (1/4:ℝ)
:=
sorry


Eric Wieser (Jan 06 2021 at 01:09):

That's a strange way to state that. Shouldn't the last two lines just be x * y \in s?

Eric Wieser (Jan 06 2021 at 01:10):

You seem to be mixing the proof with the theorem statement

Bryan Gin-ge Chen (Jan 06 2021 at 01:11):

As Kevin said, Lean reads each expression from left to right, so it has no problem realizing that a in x = a + b * ((9:ℝ) ^ (1/4:ℝ)) needs to be coerced to ℝ, since it's already seen x which is of type ℝ.

Eric Wieser (Jan 06 2021 at 01:13):

I think your statement can be proved with use [\top], ... which shows your statement is wrong

Lars Ericson (Jan 06 2021 at 01:28):

I'm trying to build up pieces of a proof that I have a subring by showing that the form a+b*I is closed under addition and multiplication where I=(9:ℝ) ^ (1/4:ℝ) and a b: ℤ. So this is a lemma about closed under multiplication. Here is an even more awkward statement of it:

import data.real.basic
import analysis.special_functions.pow

theorem ex6e_mul_closed : ∃ s : subring ℝ,
∀ x y z: ℝ,
x ∈ s →
y ∈ s →
z ∈ s →
∀ a b c d: ℤ,
x = a + b * ((9:ℝ) ^ (1/4:ℝ)) →
y = c + d * ((9:ℝ) ^ (1/4:ℝ)) →
z = x * y →
∃ e f: ℤ,
e = a * c + b * d * 3 ∧
f = a * d + b * c ∧
z = e + f * (9:ℝ) ^ (1/4:ℝ)
:=
begin
sorry
end


I am borrowing the ∃ s : subring ℝ from the theorem I want to prove which is

theorem ex6e : ∃ s : subring ℝ, ∀ x : ℝ, x ∈ s ↔ ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ) := sorry


I'm just putting it up there to get the has_pow problem to go away. It's chicken and egg though because I need to prove closed under multiplication before I have a subring, because it's part of the proof of subring.

I guess I have to rethink this and use instance or look at the structure for subring directly and prove the structure all at one time without lemmas.

Basically I need a framework where I can have a space where I prove the closed under multiplication and a space where I prove the closed under addition. I guess that's an instance.

Eric Wieser (Jan 06 2021 at 01:43):

The proof of closure is s.mul_mem for your subring lemma

Lars Ericson (Jan 06 2021 at 01:54):

That's the right idea going in the wrong direction. s.mul_mem says that if I have a subring already, then it is closed under multiplication.

I have to go the other way: I am closed under multiplication and addition, and hence I am a subring.

So net net I need to do instance: subring of some sort where what I am focusing on now is the mul_mem' and add_mem' fields of the structure, but I also have to do the other fields. It looks like I can't do these facets as separate lemmas, I have to do everything all at once. They have to be inside the proof of the instance so I can get Lean to give me has_pow between integers and reals while I am in the process of proving my subring, and not after I have proven the subring, which I can't assume because I haven't proven it yet.

Or I guess what you are saying is that Lean is coercing my integers to reals before applying has_pow. Which is OK but it is essential to the nature of what I am proving that my integers are integers "where it counts". I guess "where it counts" is when I establish that the result of addition or multiplication is of form A+B*I where A and B are definitely integers and I is definitely the real 9^(1/4).

Yakov Pechersky (Jan 06 2021 at 02:04):

You don't need an instance, you just need a structure. Your proof is the existence of such a structure. You can start your proof of an existence of such a subring (with whatever properties it has) with some statement about subring.mk' if you want.

Yakov Pechersky (Jan 06 2021 at 02:04):

Can you post an image or a latex of the actual problem statement you are formalizing?

Lars Ericson (Jan 06 2021 at 02:26):

a and b have to start life as integers. I can coerce them to real to do the multiplication with the pow, but I have to un-coerce the results of times and plus afterwards back to integer to prove the subring.

Yakov Pechersky (Jan 06 2021 at 02:31):

Try this:

import data.real.basic
import analysis.special_functions.pow

theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ (1 / 4)) ∈ s :=
begin
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
end


Yakov Pechersky (Jan 06 2021 at 02:48):

or use subring.closure _

Yakov Pechersky (Jan 06 2021 at 03:48):

But I can't make it work:

import data.real.basic
import analysis.special_functions.pow

set_option pp.all true

theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
set s : set ℝ := set.insert (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)) with hs,
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
{ exact s },
{ refine {carrier := s, one_mem' := _, mul_mem' := _},
{ rw [hs],
have := @set.mem_insert_iff ℝ 1 (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)),
rw this, -- failure, they look the same to me though
sorry
},
},
sorry
end


Yakov Pechersky (Jan 06 2021 at 03:49):

Is there some weird typo I made, or some typeclass issue?

Alex J. Best (Jan 06 2021 at 03:54):

If rw fails me I try erw instead

import data.real.basic
import analysis.special_functions.pow

--set_option pp.all true

theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
set s : set ℝ := set.insert (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)) with hs,
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
{ exact s },
{ refine {carrier := s, one_mem' := _, mul_mem' := _},
{ rw [hs],
erw set.mem_insert_iff,
},
},
sorry
end


Alex J. Best (Jan 06 2021 at 03:54):

In this case it does what you want, https://leanprover-community.github.io/mathlib_docs/tactics.html#erewrite%20/%20erw

Alex J. Best (Jan 06 2021 at 04:00):

The root cause of the issue however is that you used set.insert to define s instead of insert, quite confusing indeed.

Alex J. Best (Jan 06 2021 at 04:00):

import data.real.basic
import analysis.special_functions.pow

--set_option pp.all true

theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
set s : set ℝ := insert (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)) with hs, -- CHANGED set.insert to insert here
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
{ exact s },
{ refine {carrier := s, one_mem' := _, mul_mem' := _},
{ rw [hs],
rw set.mem_insert_iff,
},
},
sorry
end


also works then

Alex J. Best (Jan 06 2021 at 04:02):

To see this look at the last line of the error message you get from trying rw set.mem_insert_iff

rewrite tactic failed, did not find instance of the pattern in the target expression
@has_mem.mem.{?l_1 ?l_1} ?m_2 (set.{?l_1} ?m_2) (@set.has_mem.{?l_1} ?m_2) ?m_3
(@has_insert.insert.{?l_1 ?l_1} ?m_2 (set.{?l_1} ?m_2) (@set.has_insert.{?l_1} ?m_2) ?m_4 ?m_5)


its about has_insert.insert, but the goal is

 @has_mem.mem.{0 0} real (set.{0} real) (@set.has_mem.{0} real)
(@has_one.one.{0} real (@monoid.to_has_one.{0} real (@ring.to_monoid.{0} real real.ring)))
(@set.insert.{0} real ......)


which refers to set.insert instead.

Alex J. Best (Jan 06 2021 at 04:03):

These things are equal under the hood which is why erw works, but syntactically they don't look the same so rw fails.

Alex J. Best (Jan 06 2021 at 04:05):

If you look at src#set.insert you'll see it is a protected def which is maybe a bit of a hint you aren't meant to be calling it directly

Lars Ericson (Jan 06 2021 at 05:03):

Thanks for the lift. I guess as long as we know that a and b are integers in ∀ (a b : ℤ) it is fine for a to be lifted to ℝ inside the ∀. I would have thought that it was b that needed to be lifted since that is what is multiplied by the power.

I don't understand why technically you need to say s ≠ ⊤. What is ⊤, all of the reals? Because all of the reals will not be expressible as a + b * 9^(1/4) for a b : ℤ, so I don't know why the exclusion is necessary.

Yakov Pechersky (Jan 06 2021 at 05:06):

I think the formalization might be something like:

theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
refine ⟨subring.closure { 9 ^ ((1 : ℝ) / 4), (1 : ℤ) }, _, _⟩,
{ sorry },
{ sorry },
end


Yakov Pechersky (Jan 06 2021 at 05:06):

but I think there might be some lemmas missing about subring.closure to show this

Yakov Pechersky (Jan 06 2021 at 05:07):

The hs : s ≠ ⊤ is necessary because like Eric said above, the full ℝ does have the property that (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ "all of the reals".

Yakov Pechersky (Jan 06 2021 at 05:08):

And I think the exercise is to show that a strict subset of the reals is still an integral domain, or in the language here, a subring.

Lars Ericson (Jan 06 2021 at 05:18):

But 'a : ℤ', which should be enough information to exclude 's ≠ ⊤'. We know that under 'a : ℤ', the expression '(a : ℝ) + b * (9 ^ ((1 : ℝ) / 4))' is equivalent to '(a : ℤ) + b * (9 ^ ((1 : ℝ) / 4))'. The only thing stopping us from saying the latter is some technicality in Lean about no has_pow for
ℤ and ℝ together. Once you have '(a : ℤ) + b * (9 ^ ((1 : ℝ) / 4))', ⊤ is not a contender. So it shouldn't be necessary to put it in the theorem statement, because the a : ℤ in the quantifier is enough information already to exclude top.

Yakov Pechersky (Jan 06 2021 at 05:26):

When I wrote  ∀ (a b : ℤ), (a : ℝ)... that just indicates that I require a and b to be integers. They're then cast to reals.

Lars Ericson (Jan 06 2021 at 05:27):

I've moved it along a little. I should be able to apply subring.mul_mem but it is not matching although it looks exactly like it should:

import data.real.basic
import analysis.special_functions.pow

lemma one_in_Z : (1:ℝ) ∈ set.range (coe : ℤ → ℝ) :=
begin
sorry,
end

theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
set s : set ℝ := insert (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)) with hs, -- CHANGED set.insert to insert here
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
{ exact s },
{ refine {carrier := s, one_mem' := _, mul_mem' := _},
{ rw [hs],
rw set.mem_insert_iff,
right,
exact one_in_Z,
},
intros a b,
intro h1,
intro h2,
have h3 := subring.mul_mem h1 h2,
},
sorry,
sorry,
sorry,
sorry,
sorry,
end


where the goal state is

Tactic state
widget
filter:
no filter
1 goal
s: set ℝ := insert (9 ^ (1 / 4)) (set.range coe)
hs: s = insert (9 ^ (1 / 4)) (set.range coe)
ab: ℝ
h1: a ∈ s
h2: b ∈ s
⊢ a * b ∈ s


and the error is

type mismatch at application
subring.mul_mem h1
term
h1
has type
a ∈ s : Prop
but is expected to have type
subring ?m_1 : Type ?
state:
s : set ℝ := insert (9 ^ (1 / 4)) (set.range coe),
hs : s = insert (9 ^ (1 / 4)) (set.range coe),
a b : ℝ,
h1 : a ∈ s,
h2 : b ∈ s
⊢ a * b ∈ s


Yakov Pechersky (Jan 06 2021 at 05:27):

For sure, for any (a b : ℤ), a + b * (9 ^ 1 / 4) ∈ ℝ (to use set theory notation.

Yakov Pechersky (Jan 06 2021 at 05:29):

I don't think my original approach works because just inserting this 9^x value isn't enough to make that set closed. You won't be able to prove mul_mem'.

Lars Ericson (Jan 06 2021 at 05:30):

@Yakov Pechersky they are cast to reals for a technical reason, but the information in the environment, provided by the quantifier, should still include the fact that a and b are integers. You can't, to my mind, prove the subring without using that information. Completely forgetting that a is an integer forces you to say s ≠ ⊤ but that is not an insightful statement. All that is saying is "I forget that I just said that a is an integer". There should be a way of retaining that type information about a in the tactic state and then doing the coercion to make has_pow happy. It is not insightful to lose information and than replace it with another tangentially equivalent restriction.

Alex J. Best (Jan 06 2021 at 05:30):

The error message is telling you what isn't matching

type mismatch at application
subring.mul_mem h1
term
h1
has type
a ∈ s : Prop
but is expected to have type
subring ?m_1 : Type ?


the complaint is exactly that the first argument of docs#subring.mul_mem should be a subring R of some ring R, then the second and third arguments are two proofs of membership of that subring

Lars Ericson (Jan 06 2021 at 05:31):

Yes subring of R is what we are trying to prove, it is not an assumption.

Yakov Pechersky (Jan 06 2021 at 05:32):

It does remember! It'll show ↑1 for my (1 : ℤ) which is in an expression that expects an ℝ.

Alex J. Best (Jan 06 2021 at 05:34):

Lars Ericson said:

Yes subring of R is what we are trying to prove, it is not an assumption.

Right so you can't apply that lemma!

Lars Ericson (Jan 06 2021 at 05:35):

I think of a + b X where X = 9^(1/4) as a pair or a vector <a,b> where X is a kind of basis vector. The insight is that it is a ring of 2-element vectors with a slightly funny multiplication operation. The proof has to start with definition of addition and multiplication on such pairs and that such pairs multiplied or added are also pairs. The has_pow takes away from that insight, it is a kind of detour.

Lars Ericson (Jan 06 2021 at 05:37):

In other words we are spending a lot of time on coercions and has_pows and so on because we are losing sight of the idea that we have encoded integer pairs with a trick involving a single irrational real.

Lars Ericson (Jan 06 2021 at 05:40):

So 0 = <0, 0>, 1 = <1,0>, otherwise you have <a,b> where a,b are integers, and <a,b>+<c,d> = <a+c,b+d> and <a,b>*<c,d> = <a*c+*d*3, a*d+b*c>. It's really proving that pairs with that definition of + and * form a ring. The pairs are isomorphic to a + b *9^(1/4). It seems like it would be easier to prove

• The isomorphism of pairs to that expression
• That the pairs under that * and + are a ring

than to get lost in coercions between integers and reals and complicated libraries of definitions on pow.

Yakov Pechersky (Jan 06 2021 at 05:46):

This is what I mean currently:

import data.real.basic
import analysis.special_functions.pow

theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
use ⊤, -- use the whole ring of reals, the top of the subring lattice
split,
{ sorry }, -- here I am ignoring the fact I have to prove the hs hypothesis
simp
end


Yakov Pechersky (Jan 06 2021 at 05:46):

It's what Eric remarked on earlier.

Alex J. Best (Jan 06 2021 at 05:57):

Here's how I'd structure this exercise (and some of the proofs) if asked to formalise it:

import data.real.basic
import analysis.special_functions.pow

lemma important : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := begin sorry end
theorem ex6e : ∃ s : subring ℝ, (∀ x : ℝ, x ∈ s ↔ ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)) ∧ is_integral_domain s :=
begin
rw important, -- 9^1/4 is ugly, use sqrt 3 instead (likely more lemmas in library about sqrt so this will make our life easier)
refine ⟨subring.mk _ _ _ _ _ _ , ⟨_, _⟩⟩, -- separate out all the goals
rotate 6, -- we want our subring to be defined to be the a + b * (9:ℝ) ^ (1/4:ℝ)  so switch to that goal first
{ intro x,
refl, }, -- saying to lean this is true by definition forces the subring to have the elements we want, without having to do a set s := ..
rotate 1,
{ use [1,0], norm_num, }, -- 1 and 0 are easy thanks to norm num
{ sorry, }, -- this can hopefully done like the negation below, maybe using the ring, norm_num and linarith tactics.
{ use [0,0], norm_num, },
{ sorry },
{ rintro x ⟨haa, hab, rfl⟩, use [-haa, -hab], rw neg_add, simp, }, -- this is doing the "basis vector" thing lars is referring to using rintro splits our subring element x into components haa hab the rfl part clears all mention of x now we have decomposed it into its components
split,
{ use [0, 1], simp, }, -- maybe library_search does this too...
{ exact mul_comm, }, -- library_search
{ intros x y, exact mul_eq_zero.mp, }, -- library_search
end


Yakov Pechersky (Jan 06 2021 at 08:25):

Now can you do it using subring.closure { real.sqrt 3 }?

Alex J. Best (Jan 06 2021 at 08:27):

Do what, show that above criterion for membership, or show it is an integral domain?

Yakov Pechersky (Jan 06 2021 at 08:31):

Ideally, the lemmas about subring.closure should allow you to say:

refine ⟨subring.closure { real.sqrt 3 } , _, _⟩,


Alex J. Best (Jan 06 2021 at 08:35):

Oh for sure, if the goal is to formalise that same object in a easy to work with way I'd set everything up totally differently, I was just trying to match the exercise as closely as possible.

Yakov Pechersky (Jan 06 2021 at 08:43):

btw the last line can be expressed as:

  { exact @integral_domain.to_is_integral_domain _ (subring.subring.domain _) }


Yakov Pechersky (Jan 06 2021 at 08:43):

because the parent ring on ℝ is also an integral domain

Yakov Pechersky (Jan 06 2021 at 08:44):

But I guess proving that is part of the exercise

Alex J. Best (Jan 06 2021 at 08:52):

Yeah my solution is probably cheating via the typeclass mechanism really, at least in a pen and paper proof you would mention subrings of domains being domains explicitly.

Eric Wieser (Jan 06 2021 at 09:12):

@Alex J. Best' statement is the only correct one so far

Eric Wieser (Jan 06 2021 at 09:13):

The iff is crucial, otherwise it allows larger subrings than the question permits

Mario Carneiro (Jan 06 2021 at 09:39):

By the way this ring already exists in mathlib, it's called zsqrtd 3

Eric Wieser (Jan 06 2021 at 09:45):

Presumably there's some way to interpret docs#zsqrtd as asubring?

Eric Wieser (Jan 06 2021 at 09:46):

Sending it through a coercion ring hom would do the trick I assume, although I don't know where the def is for that

Eric Wieser (Jan 06 2021 at 09:47):

I'm a little surprised that zqrtd has no coercion to real...

I'll make a pr

Eric Wieser (Jan 06 2021 at 11:08):

/-- The image of zsqrtd in ℝ.  -/
@[simps]
noncomputable def to_real (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }


seems like the def needed, which proves the subring as to_real.range

Eric Wieser (Jan 06 2021 at 11:10):

I was hoping to be able to also prove

lemma to_real_injective (h : 0 ≤ d) (h_not_square : ¬∃ (x : ℤ), x*x = d) :
function.injective (to_real h) :=
(to_real h).injective_iff.mpr $λ a ha, begin simp only [to_real_apply] at ha, have : (↑a.re + ↑a.im * real.sqrt d) * (↑a.re - ↑a.im * real.sqrt d) = a.re * a.re - (real.sqrt d * real.sqrt d) * (a.im * a.im) := by ring, replace ha := congr_arg (λ x, x * (↑(a.re) - ↑(a.im) * real.sqrt ↑d)) ha, simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)] at ha, rw sub_eq_zero at ha, norm_cast at ha, simp at h_not_square, sorry, end  but I think I'm missing some knowledge of the lemmas to apply Kevin Buzzard (Jan 06 2021 at 11:51): A number-theoretic ring like $\mathbb{Z}[\sqrt{d}]$ has two maps to the reals and it's not clear to me that the one you're thinking of is any better than the other one. $\mathbb{Z}[\sqrt{d}]$ should not be thought of as a subring of the reals, it is notation for the abstract ring $\mathbb{Z}[X]/(X^2-d)$ and $X$ is no more positive than it is negative. Eric Wieser (Jan 06 2021 at 12:06): That's perhaps an argument against it being a coe, but I think the mapping should probably still exist Kevin Buzzard (Jan 06 2021 at 12:06): Both should ;-) Kevin Buzzard (Jan 06 2021 at 12:07): This is a great example of an object with a canonical non-trivial automorphism, so everything either is invariant under the automorphism or comes in pairs. Eric Wieser (Jan 06 2021 at 12:09): #5640 Eric Wieser (Jan 06 2021 at 12:09): I only added to_real because we only have real.sqrt Eric Wieser (Jan 06 2021 at 12:10): If you want the other one you can use conj.to_real Kevin Buzzard (Jan 06 2021 at 12:10): That's generally the rule when you only have one of the pair ;-) Alex J. Best (Jan 06 2021 at 12:12): alternative approach: lemma to_real_injective (h : 0 ≤ d) (h_not_square : ¬∃ (x : ℤ), x*x = d) : function.injective (to_real h) := (to_real h).injective_iff.mpr$ λ a ha, begin
simp only [to_real_apply] at ha,
have := irrational_nrt_of_notint_nrt 2 d (by sorry : (real.sqrt d) ^ 2 =d),
specialize this _ _,
by_cases haim : a.im = 0,
{ sorry },
have := rat_add a.re (rat_mul this (by exact_mod_cast haim : (a.im : ℚ) ≠ 0)),
norm_cast at this,
rw ha at this,
exfalso,
exact rat.not_irrational 0 (by exact_mod_cast this),
sorry,
sorry,
end


Eric Wieser (Jan 06 2021 at 12:18):

I've solved the lemma in the PR

Eric Wieser (Jan 06 2021 at 12:18):

So alternative approaches fine, but the bar is now sorry-free :)

Eric Wieser (Jan 06 2021 at 12:20):

@Lars Ericson, with that PR, your problem can now be solved as:

-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr

theorem ex6e : ex6 {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
sorry
end


where the final goals ought to be fairly easy to close without any knowledge of the reals

Lars Ericson (Jan 06 2021 at 14:18):

Thank you all very much. I just did a leanproject upgrade-mathlib which I guess gets me the PR. I will try to fill out the sorry in Eric's final version.

Eric Wieser (Jan 06 2021 at 14:18):

It does not get you the PR, because the PR is not merged yet!

Eric Wieser (Jan 06 2021 at 14:19):

However, you can still use the abbreviation ex6definition without the PR

Lars Ericson (Jan 06 2021 at 14:21):

It still wants has_pow:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic

-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr

theorem ex6e : ex6 {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
sorry
end


gives error

failed to synthesize type class instance for
x : ℝ,
a b : ℤ
⊢ has_pow ℝ ℝ


Eric Wieser (Jan 06 2021 at 14:21):

Yes, you need import analysis.special_functions.pow

Lars Ericson (Jan 06 2021 at 14:22):

It wants one more definition, should I add that lemma to_real_injective above?

unknown identifier 'zsqrtd.to_real'
state:
⊢ ex6 {x : ℝ | ∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)}


Eric Wieser (Jan 06 2021 at 14:23):

You don't need the injectivity one, I added that because I thought it might be useful to someone

Lars Ericson (Jan 06 2021 at 14:24):

It wants a d.

Lars Ericson (Jan 06 2021 at 14:25):

Should I add variable d: ℕ  in context?

Eric Wieser (Jan 06 2021 at 14:26):

Just add {d : ℕ} after the word to_real

Lars Ericson (Jan 06 2021 at 14:26):

I can't make it happy. This is my starting point:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

namespace zsqrtd

variable d: ℕ

/-- The image of zsqrtd in ℝ.  -/
@[simps]
noncomputable def to_real (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }

end zsqrtd

-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr

theorem ex6e : ex6 {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
sorry
end


it's giving me

type mismatch at application
int.cast_nonneg.mpr h
term
h
has type
0 ≤ d
but is expected to have type
0 ≤ ?m_1
state:
d : ℕ,
h : 0 ≤ d,
a b : ℤ√↑d,
this :
(↑(a.re) + ↑(a.im) * real.sqrt ↑d) * (↑(b.re) + ↑(b.im) * real.sqrt ↑d) =
↑(a.re) * ↑(b.re) + (↑(a.re) * ↑(b.im) + ↑(a.im) * ↑(b.re)) * real.sqrt ↑d +
↑(a.im) * ↑(b.im) * (real.sqrt ↑d * real.sqrt ↑d)
⊢ ↑((a * b).re) + ↑((a * b).im) * real.sqrt ↑d =
(↑(a.re) + ↑(a.im) * real.sqrt ↑d) * (↑(b.re) + ↑(b.im) * real.sqrt ↑d)


Eric Wieser (Jan 06 2021 at 14:27):

d should be a \Z

Lars Ericson (Jan 06 2021 at 14:27):

Thank you. This is my starting point, it checks:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

/-- The image of zsqrtd in ℝ.  -/
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }

-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr

theorem ex6e : ex6 {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
sorry
end


Eric Wieser (Jan 06 2021 at 14:28):

Great! You'll want to start by proving lemma important : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := begin sorry end.

Lars Ericson (Jan 06 2021 at 14:36):

Should be easy. I've done similar ones while golfing over last few days:

lemma nine_equals_3_times_3 : (9:ℝ) = (3:ℝ)*(3:ℝ) :=
begin
linarith,
end

lemma a_squared_equals_a_times_a (a:ℝ) : a*a = a^(2:ℕ) :=
begin
linarith,
end

lemma nine_equals_3_squared :  (9:ℝ) = ((3:ℝ) ^ (2:ℕ)) :=
begin
have h1 := nine_equals_3_times_3,
have h2 := a_squared_equals_a_times_a 3,
rw h2 at h1,
assumption,
end


Eric Wieser (Jan 06 2021 at 14:38):

a_squared_equals_a_times_a is docs#pow_two (or rather, its reverse)

Eric Wieser (Jan 06 2021 at 14:38):

Always try library_search for trivial lemmas like that first :)

Lars Ericson (Jan 07 2021 at 01:02):

How do I prove that 2 = 2? I need it for the 2nd lemma x_mul_x_pow_y_equals_x_pow_y_plus_y:

lemma two_equals_two : (2:ℕ) = (2:ℝ) :=
sorry

lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 ≤ x → (x * x)^y = x^(y+y) :=
begin
intro h,
ring,
have h1 := real.rpow_mul h (2:ℝ) y,
rw h1,
sorry,
end


The first lemma won't typecheck in the =, giving:

type mismatch at application
2 = 2
term
2
has type
ℝ
but is expected to have type
ℕ


The 2nd lemma won't go through because I have a mismatch of 2:ℕ versus 2:ℝ that I can't get rid of because the 2:ℕ is coming in under the hood without my control. Here is the goal state on the 2nd lemma:

1 goal
xy: ℝ
h: 0 ≤ x
h1: x ^ (2 * y) = (x ^ 2) ^ y
⊢ (x ^ 2) ^ y = (x ^ 2) ^ y
All Messages (8)


I should be done but the above-mentioned widget is telling me that not all 2s are alike and I don't know how to coerce my 2:N to a 2:R.

This is all in service of getting closer to the goal of proving the important lemma above. This is where I'm stuck now.

Yakov Pechersky (Jan 07 2021 at 01:06):

lemma two_equals_two : (2:ℝ) = (2:ℕ) := by norm_num


Yakov Pechersky (Jan 07 2021 at 01:06):

Not that the real has to be on the LHS for the casting to work properly.

Yakov Pechersky (Jan 07 2021 at 01:08):

You might like docs#mul_rpow

Lars Ericson (Jan 07 2021 at 01:21):

I'll try going that way. I'm using the other direction rpow_mul. The two_equals_two lemma doesn't work as a rewrite rule. I can't get this lemma to close, the goal definitely has a 2:ℕ in it but rw ← two_equals_two won't bind:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

lemma two_equals_two : (2:ℝ) = (2:ℕ) := by norm_num

lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 ≤ x → (x * x)^y = x^(y+y) :=
begin
intro h,
ring,
have h1 := real.rpow_mul h (2:ℝ) y,
have h2 := eq.symm h1,
conv
begin
to_lhs,
rw ← two_equals_two, -- FAIL
end,

end


Yakov Pechersky (Jan 07 2021 at 01:25):

Your lemma isn't true is x = 0 and y = 0

Yakov Pechersky (Jan 07 2021 at 01:28):

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

lemma two_equals_two : (2:ℝ) = (2:ℕ) := by norm_num

lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 ≤ x → 0 < y → (x * x)^y = x^(y+y) :=
begin
intros hx hy,
rw real.mul_rpow hx hx,
rcases eq_or_lt_of_le hx with rfl|hx,
{ rw real.zero_rpow (ne_of_gt hy),
rw real.zero_rpow (ne_of_gt (add_pos hy hy)),
rw zero_mul },
end


Yakov Pechersky (Jan 07 2021 at 01:35):

As you can see, no knowledge of some equality of cast nats needed.

Lars Ericson (Jan 07 2021 at 01:41):

Thanks I got there the other way but with x < 0, and no 2's using your rpow_add suggestion:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

lemma le_if_leq (x : ℝ) : 0 < x → 0 ≤ x :=
begin
intro h,
linarith,
end

lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 < x → (x * x)^y = x^(y+y) :=
begin
intro h,
have h1 := le_if_leq x h,
have h2 := @real.mul_rpow x x y h1 h1,
rw h2,
have h3 := real.rpow_add h y y,
exact eq.symm h3,
end


Yakov Pechersky (Jan 07 2021 at 01:44):

The first one is le_of_lt

Lars Ericson (Jan 07 2021 at 02:05):

@Yakov Pechersky thanks for the help. @Eric Wieser I have now proved lemma important : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 as you suggested, in only 160 lines:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

-- Eric Wieser
/-- The image of zsqrtd in ℝ.  -/
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }

-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr

lemma nine_equals_3_times_3 : (9:ℝ)=(3:ℝ)*(3:ℝ) :=
begin
linarith,
end

lemma three_is_gt_0 : (0:ℝ) < (3:ℝ) :=
begin
linarith,
end

lemma three_is_gte_0 : (0:ℝ) ≤ (3:ℝ) :=
begin
linarith,
end

lemma sqrt_of_9_is_3 : (3:ℝ) = (real.sqrt (9:ℝ)) :=
begin
have h1 := nine_equals_3_times_3,
rw h1,
have h2 := three_is_gte_0,
have h3 := real.sqrt_mul_self h2,
rw ← h1 at h3,
rw ← h1,
exact eq.symm h3,
end

lemma half_plus_half_equals_1: (1/2:ℝ)+(1/2:ℝ)=1 :=
begin
linarith,
end

lemma x_equals_sqrtx_times_sqrtx (x:ℝ): 0 < x → x = x^(1/2:ℝ) * x^(1/2:ℝ) :=
begin
intro h1,
have h3 := h2 (1/2) (1/2),
have h4 := half_plus_half_equals_1,
rw h4 at h3,
have h5 := real.rpow_one x,
rw h5 at h3,
exact h3,
end

lemma x_is_0 (x:ℝ) : x ≥ 0 → ¬(0 < x) → x = 0 :=
begin
intro h1,
intro h2,
linarith,
end

lemma half_ne_0 : (1/2:ℝ)  ≠ (0:ℝ) :=
begin
linarith,
end

lemma zero_le_0 : (0:ℝ) ≤ (0:ℝ) :=
begin
linarith,
end

lemma sqrt_0_equals_0 : real.sqrt 0 = 0 :=
begin
have h1 := zero_le_0,
exact real.sqrt_eq_zero_of_nonpos h1,
end

lemma x_gt_0_implies_sqrt_x_gt_0 (x:ℝ): x ≥ 0 → x^(1/2:ℝ) ≥ 0 :=
begin
intro h1,
exact real.rpow_nonneg_of_nonneg h1 (1 / 2),
end

lemma sqrt_x_equals_sqrt_x (x:ℝ) : x ≥ 0 → x^(1/2:ℝ) = real.sqrt x :=
begin
intro h,
have h1 := x_equals_sqrtx_times_sqrtx x,
by_cases h2 : 0 < x,
{
have h3 := h1 h2,
conv
begin
to_rhs,
rw h3,
end,
have h5 := x_gt_0_implies_sqrt_x_gt_0 x,
have h6 := h5 h,
have h4 := real.sqrt_mul_self h6,
exact eq.symm h4,
},
{
have h3 := x_is_0 x,
have h4 := h3 h,
have h5 := h4 h2,
rw h5,
have h6 := @real.zero_rpow (1/2:ℝ),
have h7 := half_ne_0,
have h8 := h6 h7,
rw h8,
have h9 := sqrt_0_equals_0,
exact eq.symm h9,
}
end

lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 < x → (x * x)^y = x^(y+y) :=
begin
intro h,
have h1 := le_of_lt h,
have h2 := @real.mul_rpow x x y h1 h1,
rw h2,
have h3 := real.rpow_add h y y,
exact eq.symm h3,
end

lemma fourth_root_of_9_equals_sqrt_sqrt : (9:ℝ) ^ (1/4:ℝ) = real.sqrt (real.sqrt (9:ℝ)) :=
begin
have h1 := nine_equals_3_times_3,
have h2 := three_is_gt_0,
have h7 := three_is_gte_0,
have h3 := sqrt_of_9_is_3,
rw ← h3,
rw h1,
have h4 := sqrt_x_equals_sqrt_x (3:ℝ),
have h5 := h4 h7,
rw ← h5,
have h6 := x_mul_x_pow_y_equals_x_pow_y_plus_y 3 (1/4),
have h8 := h6 h2,
rw h8,
ring,
end

lemma important : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 :=
begin
have h1 := fourth_root_of_9_equals_sqrt_sqrt,
rw h1,
have h2 := sqrt_of_9_is_3,
rw h2,
end


Lars Ericson (Jan 07 2021 at 02:47):

I am back to the main question, which now is how do I prove equality of two sets? Here is the context:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

-- Eric Wieser
/-- The image of zsqrtd in ℝ.  -/
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }

abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr

theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
refine omega.pred_mono_2 rfl _,
sorry,
end


Just before the sorry the goal state is:

⊢ {x : ℝ | ∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)} = ↑((zsqrtd.to_real _).range)


I don't know where to begin on how to unroll that. library_search times out and suggest gives a long list of possibilities. I haven't done any set equivalence proofs so I don't know what will reduce this to more underlying material:

Try this: refine funext _
Try this: refine eq.symm _
Try this: refine set.ext _
Try this: refine eq_comm.mp _
Try this: refine eq_comm.mpr _
Try this: refine eq_of_heq _
Try this: refine congr_arg set_of _
Try this: refine mem_id_rel.mp _
Try this: refine heq_iff_eq.mp _
Try this: refine set.ext_iff.mpr _
Try this: refine plift.up.inj _
Try this: refine ulift.up.inj _
Try this: refine let_value_eq set_of _
Try this: refine compl_inj_iff.mp _
Try this: refine (list.mem_pure {x : ℝ | ∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)}
↑((zsqrtd.to_real
(show 0 ≤ 3, from
(id (eq_true_intro (norm_num.nonneg_pos 3 (bit1_pos' zero_lt_one')))).mpr trivial)).range)).mp
_
Try this: refine setoid.ker_def.mp _
Try this: refine has_top.mk.inj _
Try this: refine has_one.mk.inj _
Try this: refine has_bot.mk.inj _
Try this: refine has_coe.mk.inj _
Try this: refine option.some_inj.mp _
Try this: refine sum.inl.inj _
Try this: refine sum.inr.inj _
Try this: refine le_antisymm _ _
Try this: refine psum.inr.inj _
Try this: refine le_antisymm' _ _
Try this: refine psum.inl.inj _
Try this: refine (divp_left_inj _).mp _
Try this: refine except.ok.inj _
Try this: refine eq.trans _ _
Try this: refine inv_unique _ _
Try this: refine neg_unique _ _
Try this: refine (eq.congr_left _).mp _
Try this: refine (eq.congr_left _).mpr _
Try this: refine is_glb.unique _ _
Try this: refine is_lub.unique _ _
Try this: refine (eq.congr_right _).mp _
Try this: refine (eq.congr_right _).mpr _
Try this: refine subtype.mk.inj _
Try this: refine (eq.congr _ _).mp _
Try this: refine (eq.congr _ _).mpr _
Try this: refine pequiv.inj _ _ _
Try this: refine one_hom.mk.inj _
Try this: refine rel_hom.mk.inj _
Try this: refine mul_hom.mk.inj _
Try this: refine zero_hom.mk.inj _
Try this: refine subgroup.mk.inj _
Try this: refine subring.mk.inj _
Try this: refine alg_hom.mk.inj _


Mario Carneiro (Jan 07 2021 at 06:30):

Yakov Pechersky said:

lemma two_equals_two : (2:ℝ) = (2:ℕ) := by norm_num


I think simp is doing all the work there

Eric Wieser (Jan 07 2021 at 07:45):

I have no idea what docs#omega.pred_mono_2 is, but I'm pretty sure you don't want to use it - it's undoing the progress made by ext

Lars Ericson (Jan 07 2021 at 17:46):

Thanks, per @Floris van Doorn I backed out the omega and applied docs#set.mem_set_of_eq and that gets me here which gets me back into predicate calculus and out of sets:

⊢ (∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)) ↔ x ∈ ↑((zsqrtd.to_real _).range)


I don't see that in the suggest list, so that's a possible improvement for suggest.

Alex J. Best (Jan 07 2021 at 18:01):

You can always do suggest 100 to get more suggestions, perhaps it shows up with a higher number than the default?

Lars Ericson (Jan 09 2021 at 04:38):

I got it this far but I'm out of ideas again:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

/-- The image of zsqrtd in ℝ.  -/  -- Eric Wieser
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }

abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr

lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := sorry

theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw set.mem_set_of_eq,
split,
{
intro h1,
apply exists.intro,
split,
{
cases h1 with a ha,
cases ha with b hb,
exact trivial,
},
{
cases h1 with a ha,
cases ha with b hb,
norm_num,
have h2 := fourth_root_of_nine_equals_sqrt_3,
rw ← h2,
sorry,
},
exact zsqrtd.one,
},
{
intro h,
apply exists.intro,
apply exists.intro,
cases h,
unfold_coes,
sorry,
exact int.one,
exact int.one,
}
end


At the first sorry, my tactic state is

1 goal
x: ℝ
ab: ℤ
hb: x = ↑a + ↑b * 9 ^ (1 / 4)
h2: 9 ^ (1 / 4) = real.sqrt 3
⊢ ↑(?m_1[_].re) + ↑(?m_1[_].im) * 9 ^ (1 / 4) = x


It's asking for real and imaginary parts of an unmatched thing. I haven't been reasoning about complex numbers, that just popped up.

The second sorry also seems to want me to fill in some random number. The goal state is

3 goals
x: ℝ
h_w: ℤ√3
h_h: h_w ∈ ⊤.carrier ∧ ⇑(zsqrtd.to_real _) h_w = x
⊢ x = int.cast ?m_1[_] + int.cast ?m_2[_] * 9 ^ (1 / 4)


I don't understand how to work with these metavariables and what the tactics or theorems are that would apply.

Thomas Browning (Jan 09 2021 at 04:44):

things seem to start to go wrong at apply exists.intro

Mario Carneiro (Jan 09 2021 at 04:46):

This seems like a good starting point

theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
sorry
end


Mario Carneiro (Jan 09 2021 at 04:46):

the proof of the sorry should be very short, just unpacking and repacking the real and imaginary parts

Thomas Browning (Jan 09 2021 at 04:47):

By the way, the re and im aren't actually referring to complex numbers here

Thomas Browning (Jan 09 2021 at 04:47):

If you look at zsqrtd/basic.lean, you see this:

/-- The ring of integers adjoined with a square root of d.
These have the form a + b √d where a b : ℤ. The components
are called re and im by analogy to the negative d case,
but of course both parts are real here since d is nonnegative. -/
structure zsqrtd (d : ℤ) :=
(re : ℤ)
(im : ℤ)


Thomas Browning (Jan 09 2021 at 04:48):

so the re and im are referring to the a and the b in a + b √d

Lars Ericson (Jan 09 2021 at 14:38):

I have reached an absurdity. It is asking me to prove ⊢ a = b ∨ real.sqrt 3 = 0 after the simp *:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

/-- The image of zsqrtd in ℝ.  -/  -- Eric Wieser
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }

abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr

lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := sorry

theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
split,
{
intro h1,
cases h1 with a ha,
cases ha with b hb,
apply exists.intro,
rw hb,
rotate,
exact {re := a, im := a},
simp *,
-- ⊢ a = b ∨ real.sqrt 3 = 0
},
{
sorry,
}
end


Kevin Buzzard (Jan 09 2021 at 14:40):

Do you know the maths proof of what you're trying to prove? Lean won't figure out the ideas, it will just check them.

Eric Wieser (Jan 09 2021 at 14:44):

I think the maths proof by the time you reach the split is "both sides are obviously the same"

Eric Wieser (Jan 09 2021 at 14:45):

But in this case, your mistake is the exact line

Eric Wieser (Jan 09 2021 at 14:46):

It should read im := b

Lars Ericson (Jan 09 2021 at 14:50):

@Kevin Buzzard what I actually wanted to prove is that the ring is closed under addition and multiplication as defined by <a,b>+<c,d>=<a+b,c+d> and <a,b>*<c,d> = <a*c+3*b*d, a*d+b*c>. In the recent above I am following expert suggestions which do not map directly to my original intuition.

Lars Ericson (Jan 09 2021 at 14:51):

@Eric Wieser I don't know the syntax to assign directly to the components of the goal. This doesn't work:

exact { im := b },


where the goal is

⊢ ↑(?m_1.re) + ↑(?m_1.im) * real.sqrt 3 = ↑a + ↑b * real.sqrt 3


Eric Wieser (Jan 09 2021 at 14:57):

You already have im := a in your example code

Eric Wieser (Jan 09 2021 at 14:57):

Just change the a for a b

Eric Wieser (Jan 09 2021 at 14:57):

congr would probably also solve that goal

Eric Wieser (Jan 09 2021 at 15:02):

I think apply exists.intro is a recurring wrong choice you seen to be taking. When you're faced with an existential, your strategy should be to think of the maths proof and work out which object to provide; then use tactic#use

Lars Ericson (Jan 09 2021 at 16:16):

Thank you @Eric Wieser I will follow the advice on exists.intro.

Lars Ericson (Jan 09 2021 at 18:37):

I got farther on the first half of the split.

On the second half, I'm trying to make y=0 + 0 * sqrt(3) and apply it on the exist which is in the assumptions. It's not going through, I don't know the syntax:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

/-- The image of zsqrtd in ℝ.  -/  -- Eric Wieser
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }

abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr

lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := sorry

theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
split,
{
intro h1,
cases h1 with a ha,
cases ha with b hb,
use {re := a, im := b},
rw hb,
},
{
intro h,
use 0,
use 0,
simp *,
have y : ℤ√3 := {re := 0, im := 0},
have h3 := h y, -- ERROR
}
end


The goal state is

x: ℝ
h: ∃ (y : ℤ√3), ↑(y.re) + ↑(y.im) * real.sqrt 3 = x
y: ℤ√3
⊢ x = 0


Eric Wieser (Jan 09 2021 at 18:46):

Why did you use 0?

Eric Wieser (Jan 09 2021 at 18:49):

Your goal state is unprovable because you used the wrong value

Eric Wieser (Jan 09 2021 at 18:50):

What was the goal state before the first use 0?

Lars Ericson (Jan 09 2021 at 20:36):

I'm at this tactic state:

1 goal
x: ℝ
y: ℤ√3
hy: ↑(y.re) + ↑(y.im) * real.sqrt 3 = x
⊢ ∃ (a b : ℤ), ↑(y.re) + ↑(y.im) * real.sqrt 3 = ↑a + ↑b * real.sqrt 3


I want to set y.re to a and y.im to b. using something like

have y:ℤ√3 := a + b * real.sqrt 3,


and have that get applied to the goal to replace y.re with a and y.im with b. I don't know how to do it. This is just before the sorry in

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

/-- The image of zsqrtd in ℝ.  -/  -- Eric Wieser
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }

abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr

lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := sorry

theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
split,
{
intro h1,
cases h1 with a ha,
cases ha with b hb,
use {re := a, im := b},
rw hb,
},
{
intro h1,
cases h1 with y hy,
rw ← hy,
sorry
}
end


Eric Wieser (Jan 09 2021 at 21:18):

use [y.re, y.im]

Lars Ericson (Jan 09 2021 at 22:51):

Exercise 6E, we hardly knew ye:

import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

-- Eric Wieser
/-- The image of zsqrtd in ℝ.  -/
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }

-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr

lemma nine_equals_3_times_3 : (9:ℝ)=(3:ℝ)*(3:ℝ) :=
begin
linarith,
end

lemma three_is_gt_0 : (0:ℝ) < (3:ℝ) :=
begin
linarith,
end

lemma three_is_gte_0 : (0:ℝ) ≤ (3:ℝ) :=
begin
linarith,
end

lemma sqrt_of_9_is_3 : (3:ℝ) = (real.sqrt (9:ℝ)) :=
begin
have h1 := nine_equals_3_times_3,
rw h1,
have h2 := three_is_gte_0,
have h3 := real.sqrt_mul_self h2,
rw ← h1 at h3,
rw ← h1,
exact eq.symm h3,
end

lemma half_plus_half_equals_1: (1/2:ℝ)+(1/2:ℝ)=1 :=
begin
linarith,
end

lemma x_equals_sqrtx_times_sqrtx (x:ℝ): 0 < x → x = x^(1/2:ℝ) * x^(1/2:ℝ) :=
begin
intro h1,
have h3 := h2 (1/2) (1/2),
have h4 := half_plus_half_equals_1,
rw h4 at h3,
have h5 := real.rpow_one x,
rw h5 at h3,
exact h3,
end

lemma x_is_0 (x:ℝ) : x ≥ 0 → ¬(0 < x) → x = 0 :=
begin
intro h1,
intro h2,
linarith,
end

lemma half_ne_0 : (1/2:ℝ)  ≠ (0:ℝ) :=
begin
linarith,
end

lemma zero_le_0 : (0:ℝ) ≤ (0:ℝ) :=
begin
linarith,
end

lemma sqrt_0_equals_0 : real.sqrt 0 = 0 :=
begin
have h1 := zero_le_0,
exact real.sqrt_eq_zero_of_nonpos h1,
end

lemma x_gt_0_implies_sqrt_x_gt_0 (x:ℝ): x ≥ 0 → x^(1/2:ℝ) ≥ 0 :=
begin
intro h1,
exact real.rpow_nonneg_of_nonneg h1 (1 / 2),
end

lemma sqrt_x_equals_sqrt_x (x:ℝ) : x ≥ 0 → x^(1/2:ℝ) = real.sqrt x :=
begin
intro h,
have h1 := x_equals_sqrtx_times_sqrtx x,
by_cases h2 : 0 < x,
{
have h3 := h1 h2,
conv
begin
to_rhs,
rw h3,
end,
have h5 := x_gt_0_implies_sqrt_x_gt_0 x,
have h6 := h5 h,
have h4 := real.sqrt_mul_self h6,
exact eq.symm h4,
},
{
have h3 := x_is_0 x,
have h4 := h3 h,
have h5 := h4 h2,
rw h5,
have h6 := @real.zero_rpow (1/2:ℝ),
have h7 := half_ne_0,
have h8 := h6 h7,
rw h8,
have h9 := sqrt_0_equals_0,
exact eq.symm h9,
}
end

lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 < x → (x * x)^y = x^(y+y) :=
begin
intro h,
have h1 := le_of_lt h,
have h2 := @real.mul_rpow x x y h1 h1,
rw h2,
have h3 := real.rpow_add h y y,
exact eq.symm h3,
end

lemma fourth_root_of_9_equals_sqrt_sqrt : (9:ℝ) ^ (1/4:ℝ) = real.sqrt (real.sqrt (9:ℝ)) :=
begin
have h1 := nine_equals_3_times_3,
have h2 := three_is_gt_0,
have h7 := three_is_gte_0,
have h3 := sqrt_of_9_is_3,
rw ← h3,
rw h1,
have h4 := sqrt_x_equals_sqrt_x (3:ℝ),
have h5 := h4 h7,
rw ← h5,
have h6 := x_mul_x_pow_y_equals_x_pow_y_plus_y 3 (1/4),
have h8 := h6 h2,
rw h8,
ring,
end

lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 :=
begin
have h1 := fourth_root_of_9_equals_sqrt_sqrt,
rw h1,
have h2 := sqrt_of_9_is_3,
rw h2,
end

abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr

theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
split,
{
intro h1,
cases h1 with a ha,
cases ha with b hb,
use {re := a, im := b},
rw hb,
},
{
intro h1,
cases h1 with y hy,
rw ← hy,
use [y.re, y.im],
}
end


Kevin Buzzard (Jan 09 2021 at 23:20):

I think it's easier if you just do it directly without using this zsqrtd stuff:

import tactic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow

abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr

open real

lemma useful : ((9 : ℝ) ^ (4⁻¹ : ℝ)) * (9 ^ (4⁻¹ : ℝ)) = 3 :=
begin
rw ← mul_rpow,
convert pow_nat_rpow_nat_inv (show (0 : ℝ) ≤ 3, by norm_num) (show 0 < 4, by norm_num) using 2,
all_goals {norm_num}
end

def A : subring ℝ :=
{ carrier := {x | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)},
one_mem' := ⟨1, 0, by simp⟩,
mul_mem' := begin
rintro _ _ ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩,
use [a1 * a2 + 3 * b1 * b2, a1 * b2 + a2 * b1],
ring,
end,
zero_mem' := ⟨0, 0, by simp⟩,
add_mem' := by { rintro _ _ ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩,
use [a1 + a2, b1 + b2],
simp, ring },
neg_mem' := by { rintro _ ⟨a, b, rfl⟩,
use [-a, -b],
simp, ring },
}

noncomputable instance : integral_domain A := by apply_instance

theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
⟨A, infer_instance, rfl⟩


Kevin Buzzard (Jan 09 2021 at 23:30):

This way you just isolate the useful lemma and you don't ever need to engage with square roots at all.

Mario Carneiro (Jan 09 2021 at 23:31):

I disagree. The first lemma by Eric is supposed to be in mathlib (I think it's PR'd), and the rest is a few lines

Kevin Buzzard (Jan 09 2021 at 23:36):

Fair enough. My construction of the subring shouldn't be in mathlib and that's most of the work. I guess your way you still need to prove 9^{1/4}=sqrt(3), that just looked unappealing to me for some reason, but now I see we already have sqrt_eq_rpow

Kevin Buzzard (Jan 09 2021 at 23:39):

BTW we're missing pow_inj : a^x=b^x -> a=b (modulo edge cases) (at least as far as I can see)

Mario Carneiro (Jan 09 2021 at 23:50):

theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw calc (9:ℝ) ^ (1/4:ℝ) = (9:ℝ)^((2:ℕ)⁻¹ * (1/2) : ℝ) : by norm_num
... = ((3^2:ℝ)^((2:ℕ)⁻¹:ℝ)) ^ (1/2:ℝ) : by rw real.rpow_mul; norm_num
... = real.sqrt 3 : by rw [real.pow_nat_rpow_nat_inv, real.sqrt_eq_rpow]; norm_num,
simp [zsqrtd.to_real],
exact ⟨λ ⟨x,y,h⟩, ⟨⟨x,y⟩, h.symm⟩, λ ⟨⟨x,y⟩,h⟩, ⟨x,y, h.symm⟩⟩,
end


Lars Ericson (Jan 09 2021 at 23:51):

Kevin's proof is easier for me to follow because it directly constructs the subring.

Kevin Buzzard (Jan 09 2021 at 23:51):

Mario's proof is the same as yours, he just gets to the point more directly.

Mario Carneiro (Jan 09 2021 at 23:53):

There certainly seems to be some friction around real.rpow that could use some automation

Kevin Buzzard (Jan 09 2021 at 23:53):

I don't think I've ever seen rw calc before, and it doesn't seem to ever occur in mathlib.

Mario Carneiro (Jan 09 2021 at 23:53):

It would be rw show but calc kind of has show built in

Nice!

Eric Wieser (Jan 10 2021 at 00:40):

@Lars Ericson, the point of my approach to the proof is that mathlib already has the ring construction so there is no need to build it yourself

Eric Wieser (Jan 10 2021 at 00:40):

Pedagogically of course, you can still do so

Lars Ericson (Jan 10 2021 at 01:09):

@Eric Wieser , I'm grateful for your help. In this example, the relevant subring was already mostly in mathlib, except for the multiplication which you define in zsqrtd.to_real. For a beginner like myself, to transfer the techniques to a subring which is not already in mathlib, the pattern of def A seems easier to replicate.

Eric Wieser (Jan 27 2021 at 22:47):

docs#zsqrtd.to_real is now merged

Last updated: May 17 2021 at 22:15 UTC