Zulip Chat Archive

Stream: new members

Topic: How to multiply an integer times a real


view this post on Zulip 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

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

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

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Jan 06 2021 at 01:10):

You seem to be mixing the proof with the theorem statement

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

view this post on Zulip Eric Wieser (Jan 06 2021 at 01:13):

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

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

view this post on Zulip Eric Wieser (Jan 06 2021 at 01:43):

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

view this post on Zulip 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).

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 02:04):

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

view this post on Zulip Lars Ericson (Jan 06 2021 at 02:23):

6E:
Screenshot-from-2021-01-05-21-23-27.png

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 02:48):

or use subring.closure _

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 03:49):

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

view this post on Zulip 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

view this post on Zulip 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

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

view this post on Zulip 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

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

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

view this post on Zulip 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

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 05:06):

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

view this post on Zulip 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".

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

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

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 05:27):

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

view this post on Zulip 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'.

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

view this post on Zulip 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

view this post on Zulip Lars Ericson (Jan 06 2021 at 05:31):

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

view this post on Zulip 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 ℝ.

view this post on Zulip 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!

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

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

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 05:46):

It's what Eric remarked on earlier.

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 08:25):

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

view this post on Zulip Alex J. Best (Jan 06 2021 at 08:27):

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

view this post on Zulip 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 } , _, _⟩,

instead

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

view this post on Zulip 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 _) }

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 08:43):

because the parent ring on is also an integral domain

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 08:44):

But I guess proving that is part of the exercise

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

view this post on Zulip Eric Wieser (Jan 06 2021 at 09:12):

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

view this post on Zulip Eric Wieser (Jan 06 2021 at 09:13):

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

view this post on Zulip Mario Carneiro (Jan 06 2021 at 09:39):

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

view this post on Zulip Eric Wieser (Jan 06 2021 at 09:45):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 06 2021 at 09:47):

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

view this post on Zulip Alex J. Best (Jan 06 2021 at 09:50):

Well according to the copyright headers its older than real :grinning:

view this post on Zulip Eric Wieser (Jan 06 2021 at 09:59):

I'll make a pr

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 06 2021 at 11:51):

A number-theoretic ring like Z[d]\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. Z[d]\mathbb{Z}[\sqrt{d}] should not be thought of as a subring of the reals, it is notation for the abstract ring Z[X]/(X2d)\mathbb{Z}[X]/(X^2-d) and XX is no more positive than it is negative.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 06 2021 at 12:06):

Both should ;-)

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

view this post on Zulip Eric Wieser (Jan 06 2021 at 12:09):

#5640

view this post on Zulip Eric Wieser (Jan 06 2021 at 12:09):

I only added to_real because we only have real.sqrt

view this post on Zulip Eric Wieser (Jan 06 2021 at 12:10):

If you want the other one you can use conj.to_real

view this post on Zulip Kevin Buzzard (Jan 06 2021 at 12:10):

That's generally the rule when you only have one of the pair ;-)

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 06 2021 at 12:18):

I've solved the lemma in the PR

view this post on Zulip Eric Wieser (Jan 06 2021 at 12:18):

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

view this post on Zulip 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

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

view this post on Zulip Eric Wieser (Jan 06 2021 at 14:18):

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

view this post on Zulip Eric Wieser (Jan 06 2021 at 14:19):

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

view this post on Zulip 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  

view this post on Zulip Eric Wieser (Jan 06 2021 at 14:21):

Yes, you need import analysis.special_functions.pow

view this post on Zulip 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)}

view this post on Zulip Eric Wieser (Jan 06 2021 at 14:23):

You need this one: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20to.20multiply.20an.20integer.20times.20a.20real/near/221755534

view this post on Zulip 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

view this post on Zulip Lars Ericson (Jan 06 2021 at 14:24):

It wants a d.

view this post on Zulip Lars Ericson (Jan 06 2021 at 14:25):

Should I add variable d: ℕ in context?

view this post on Zulip Eric Wieser (Jan 06 2021 at 14:26):

Just add {d : ℕ} after the word to_real

view this post on Zulip 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)

view this post on Zulip Eric Wieser (Jan 06 2021 at 14:27):

d should be a \Z

view this post on Zulip 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

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 06 2021 at 14:38):

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

view this post on Zulip Eric Wieser (Jan 06 2021 at 14:38):

Always try library_search for trivial lemmas like that first :)

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:06):

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:06):

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:08):

You might like docs#mul_rpow

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:25):

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

view this post on Zulip 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 },
  { rw real.rpow_add hx }
end

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:35):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:44):

The first one is le_of_lt

view this post on Zulip 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 h2 := real.rpow_add 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

view this post on Zulip 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 add_hom.mk.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 _

view this post on Zulip 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

view this post on Zulip 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

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

view this post on Zulip 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?

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

view this post on Zulip Thomas Browning (Jan 09 2021 at 04:44):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Thomas Browning (Jan 09 2021 at 04:47):

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

view this post on Zulip 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 : )

view this post on Zulip 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

view this post on Zulip 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

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

view this post on Zulip 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"

view this post on Zulip Eric Wieser (Jan 09 2021 at 14:45):

But in this case, your mistake is the exact line

view this post on Zulip Eric Wieser (Jan 09 2021 at 14:46):

It should read im := b

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 09 2021 at 14:57):

You already have im := a in your example code

view this post on Zulip Eric Wieser (Jan 09 2021 at 14:57):

Just change the a for a b

view this post on Zulip Eric Wieser (Jan 09 2021 at 14:57):

congr would probably also solve that goal

view this post on Zulip 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

view this post on Zulip Lars Ericson (Jan 09 2021 at 16:16):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 09 2021 at 18:46):

Why did you use 0?

view this post on Zulip Eric Wieser (Jan 09 2021 at 18:49):

Your goal state is unprovable because you used the wrong value

view this post on Zulip Eric Wieser (Jan 09 2021 at 18:50):

What was the goal state before the first use 0?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 09 2021 at 21:18):

use [y.re, y.im]

view this post on Zulip 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 h2 := real.rpow_add 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

view this post on Zulip 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],
    simp [mul_add, add_mul, mul_assoc, mul_left_comm, useful],
    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

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Lars Ericson (Jan 09 2021 at 23:51):

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

view this post on Zulip Kevin Buzzard (Jan 09 2021 at 23:51):

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

view this post on Zulip Mario Carneiro (Jan 09 2021 at 23:53):

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

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

view this post on Zulip Mario Carneiro (Jan 09 2021 at 23:53):

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

view this post on Zulip Kevin Buzzard (Jan 09 2021 at 23:54):

Nice!

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 10 2021 at 00:40):

Pedagogically of course, you can still do so

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

view this post on Zulip Eric Wieser (Jan 27 2021 at 22:47):

docs#zsqrtd.to_real is now merged


Last updated: May 17 2021 at 22:15 UTC