Stream: quantum computing

Topic: quantum Fourier transform


view this post on Zulip Anthony Bordg (Jul 04 2019 at 13:31):

@Yijun He I'm going to work on the sorry you temporarily left.

view this post on Zulip Anthony Bordg (Jul 04 2019 at 14:57):

@Yijun He There might be a problem with the first sorry in qft_no_swap_of_unit_vec. Maybe some additional assumptions are needed. Please see the attached file with my comments.
Quantum_Fourier_Transform_draft.thy

view this post on Zulip Yijun He (Jul 04 2019 at 15:06):

Yes I also found it, and I just pushed a fix to my fork

view this post on Zulip Yijun He (Jul 04 2019 at 15:11):

I also have a question about induction: how can I impose a restriction to the induction variable? For example, I want to induct in the range 0 <= m <= n-1, but using "proof (induction m)" stops me from using the assumption "m<n" in case (Suc m), since m is already specified in this case

view this post on Zulip Anthony Bordg (Jul 04 2019 at 15:20):

@Yijun He The fastest method to get an answer to your question is to ask Larry before he leaves his office at 5pm! :running:

view this post on Zulip Yijun He (Jul 04 2019 at 15:24):

It seems that he is not in his office today :sweat:

view this post on Zulip Anthony Bordg (Jul 04 2019 at 15:39):

@Yijun He OK, I had no luck with the documentation. For an induction on mm with the specified range, in the case Suc m you should be able to use m<n1 m < n-1, not m<nm<n, so Isabelle is right. Can you ask the mailing list (Distribution & Support) ?

view this post on Zulip Yijun He (Jul 04 2019 at 16:17):

I found a way to use the assumption just now, but it looks a bit messy: I added "m>n or..." to the induction hypothesis of qft_no_swap_of_unit_vec, which allows me to trivially say "m > n ==> (Suc m) > n" when m is greater than n.

view this post on Zulip Anthony Bordg (Jul 05 2019 at 21:16):

@Yijun He ind_from_1 and its use in pow_tensor_dim_row by @Hanna Lachnitt in her theory Deutsch_Jozsa.thy might be a source of inspiration wrt the problem we discuss earlier.

view this post on Zulip Anthony Bordg (Jul 06 2019 at 14:33):

@Yijun He I'm going to take care of the simplification of uniq_select_index.

view this post on Zulip Anthony Bordg (Jul 08 2019 at 13:52):

@Yijun He In uniq_select_index I'm thinking about refactoring the statement ⋀a. (a∈{..<n+1} ⟹ i mod (2^a) = j mod (2^a)) under the appropriate assumptions. Do you think it might be a useful lemma on its own ?

view this post on Zulip Yijun He (Jul 08 2019 at 13:54):

I am not sure about that

view this post on Zulip Yijun He (Jul 08 2019 at 13:56):

That statement requires the assumption that ⋀a. (a∈{..<n} ⟹ select_index n a i = select_index n a j), which seems too specific

view this post on Zulip Anthony Bordg (Jul 08 2019 at 13:58):

Ok, in that case I don't see a way to shorten the proof by refactoring or changing its structure. But at least I can try to clean the proof of ⋀a. (a∈{..<n+1} ⟹ i mod (2^a) = j mod (2^a)) which seems the longest step.

view this post on Zulip Yijun He (Jul 08 2019 at 13:59):

OK, thanks!

view this post on Zulip Anthony Bordg (Jul 08 2019 at 14:02):

On the other hand, it's true that ⋀a. (a∈{..<n} ⟹ select_index n a i = select_index n a j) is specific, but refactoring may be the first step towards putting all this fancy stuff about select_index into a dedicated theory, or even into a specific section of the Basics theory.

view this post on Zulip Yijun He (Jul 08 2019 at 14:06):

That might be a better solution, as it is indeed a basic/intuitive result of number theory/modular arithmetic

view this post on Zulip Anthony Bordg (Jul 08 2019 at 14:11):

Of course, in that case we can directly put the whole proof uniq_select_index somewhere else, but I still feel the proof is too long. Also, somewhere else we might have burried some lemmas related to select_index inside proofs. In that case, refactoring and then putting that stuff in a dedicated place is the way to go.

view this post on Zulip Anthony Bordg (Jul 08 2019 at 15:01):

@Yijun He Inside the syntax case (Suc a) you can't write a + 1, but everywhere else in the proof note that you can and should write a + 1, since we do not want the code to feel alien for any ordinary mathematician.

view this post on Zulip Yijun He (Jul 08 2019 at 15:06):

I am not sure why, but sometimes auto might fail when I change Suc k to k+1 (and sometimes it works properly).

view this post on Zulip Anthony Bordg (Jul 08 2019 at 15:07):

In that specific case I had no trouble with auto. :slight_smile:

view this post on Zulip Yijun He (Jul 08 2019 at 15:10):

OK, I will change it to k + 1 whenever possible.

view this post on Zulip Anthony Bordg (Jul 08 2019 at 15:11):

I did it for uniq_select_index.

view this post on Zulip Anthony Bordg (Jul 08 2019 at 15:30):

So, keep Suc k if for whatever reason you have some trouble and write k + 1 whenever possible.

view this post on Zulip Anthony Bordg (Jul 08 2019 at 18:53):

@Yijun He I cleaned the proof of uniq_select_index (please see my PR). From that proof I factored out two lemmas mod_pow_2_eq and select_index_eq_to_mod_eq. It's unlikely that select_index_eq_to_mod_eq will be useful in the future, but I believe mod_pow_2_eq may be useful. Also, the whole thing is now much more legible than previously.

view this post on Zulip Yijun He (Jul 09 2019 at 13:45):

@Anthony Bordg I am currently struggling with the complicated expressions in quantum Fourier transform. In the book, the vectors are expressed as the tensor product of n qubits, but I am not sure about how to do that in Isabelle (product and sum require the operators to be comm_monoid, which doesn't work for tensor product and even vector addition), and my current expressions using products and select_index seems too complicated to work with. Could you give me some advice about it? Many thanks.

view this post on Zulip Anthony Bordg (Jul 09 2019 at 13:58):

@Yijun He vector addition is obviously a monoid law (for any given dimension), so I would be very surprised if it's not already proven, and if it's not then we need to prove it.

view this post on Zulip Yijun He (Jul 09 2019 at 14:05):

For example, when I try to make a statement "v = (∑k<n. unit_vec n k)" (this is incorrect, but the variable types should be correct), Isabelle gives an error message saying No type arity Matrix.vec :: comm_monoid_add

view this post on Zulip Anthony Bordg (Jul 09 2019 at 14:07):

Can I find your draft on GitHub ? Otherwise, please send me your file.

view this post on Zulip Yijun He (Jul 09 2019 at 14:10):

I just pushed my updates to GitHub.

view this post on Zulip Yijun He (Jul 09 2019 at 14:11):

I added a test lemma sum_of_unit_vec, which uses the exact statement above and should give an error message.

view this post on Zulip Anthony Bordg (Jul 09 2019 at 14:21):

unit_vec n k is of type complex Matrix.vec. Now, if you look at the theory Matrix.thy, you see the lemma comm_monoid_vec, where the locale comm_monoid is introduced in Group.thy. But, comm_monoid_add is a class introduced in Groups.thy.

view this post on Zulip Anthony Bordg (Jul 09 2019 at 14:24):

So, it's enough to prove comm_monoid_add of the set of complex vectors of a given dimension. I will do that.

view this post on Zulip Yijun He (Jul 09 2019 at 14:26):

thanks!

view this post on Zulip Jose Manuel Rodríguez Caballero (Jul 09 2019 at 14:29):

Just to show a different approach. My solution for expressing "v = (∑k<n. unit_vec n k)" would be to go from "complex vec" to "nat ell2" using my function "vec_to_ell2". The type "nat ell2" is the complex Hilbert space of square-summable sequences of complex numbers (in particular comm_monoid). In order to return to "complex vec" from "nat ell2", I use the function "ell2_to_vec". Indeed, "unit_vec n k" goes to what I call "ket k" in "nat ell2". Finite_Dimensional_Case.thy

view this post on Zulip Anthony Bordg (Jul 09 2019 at 15:14):

@Yijun He Even better, I browsed the theory Matrix.thy and I discovered that one has the definition finsum_vec. I think this is the definition you want to use here and the corresponding lemmas they proved to handle such sums.

view this post on Zulip Yijun He (Jul 09 2019 at 15:31):

finsum_vec seems to work now. Many thanks!

view this post on Zulip Anthony Bordg (Jul 09 2019 at 15:32):

The only thing lacking is a nice notation like \sum for finsum_vec, but we can introduce it as an abbreviation.

view this post on Zulip Anthony Bordg (Jul 17 2019 at 21:54):

@Yijun He About the use of Suc n vs n+1 Part 2 of the style guide (7th bullet) seems to have a point when it says that it depends on the distinction between top-level lemmas that you may want to present to people and lemmas that are used in further proofs as a convenient scaffolding in the formalization process. For the latter, normal forms are fine and may help automation.

view this post on Zulip Anthony Bordg (Jul 19 2019 at 13:33):

@Yijun He This afternoon I plan to work on the proof of qubits_tensor_prod. Is that ok with you ?

view this post on Zulip Yijun He (Jul 19 2019 at 13:37):

That would be great, thanks! Actually it still needs some assumptions on the functions f and g's. I am still working on the proof of qft_no_swap_of_unit_vec.

view this post on Zulip Anthony Bordg (Jul 20 2019 at 16:27):

@Yijun He done. But, for the proof the associativity of the tensor product of matrices is needed. So, I'm going to prove this associativity in Tensor.thy.

view this post on Zulip Anthony Bordg (Jul 20 2019 at 22:30):

@Yijun He Probably due to the changes in Binary_Nat.thy your proof of select_index_eq_bin_rep is broken. The bad thing: I don't get a proof without smt.

view this post on Zulip Anthony Bordg (Jul 20 2019 at 22:39):

@Yijun He In qubits_rep I changed select_index n j i to select_index n i j (and made the corresponding changes).
Indeed, in Quantum.thy select_index is defined as

select_index n i j ≡ (i≤n-1) ∧ (j≤2^n - 1) ∧ (j mod 2^(n-i) ≥ 2^(n-1-i)).

It's confusing to use the same letters but with a permutation.

view this post on Zulip Anthony Bordg (Jul 21 2019 at 09:32):

Associativity for the tensor product of complex matrices done.

view this post on Zulip Anthony Bordg (Jul 21 2019 at 10:33):

@Yijun He I made a PR in your master branch. Also, Tensor.thy is up-to-date in my master branch.

view this post on Zulip Yijun He (Jul 21 2019 at 10:37):

Thanks! Pull request merged.

view this post on Zulip Anthony Bordg (Jul 22 2019 at 14:32):

@Yijun He Please tell me which sorry you want me to tackle next.

view this post on Zulip Yijun He (Jul 22 2019 at 14:36):

Maybe the sorry in qft_no_swap_of_unit_vec? Now I am not even sure whether my formulation is correct. Many thanks.

view this post on Zulip Anthony Bordg (Jul 22 2019 at 14:39):

Ok, in that case I will work on the first sorry in qft_no_swap_of_unit_vec.

view this post on Zulip Anthony Bordg (Jul 22 2019 at 15:29):

@Yijun He In the book what is the corresponding element to qft_no_swap n m v ?

view this post on Zulip Yijun He (Jul 22 2019 at 15:32):

It should be an intermediate state of the expression (5.17), where v is the unit vector |j⟩.

view this post on Zulip Anthony Bordg (Jul 26 2019 at 14:29):

@Yijun He We have to do some reverse engineering here if we have Shor's algorithm in mind. To what extent do we need the quantum Fourier Transform to formalize Shor's algorithm ?

view this post on Zulip Yijun He (Jul 26 2019 at 14:41):

Proving correctness of Shor's algorithm seems to need the correctness of inverse Quantum Fourier Transform.

view this post on Zulip Anthony Bordg (Jul 26 2019 at 14:48):

Proving correctness of Shor's algorithm seems to need the correctness of inverse Quantum Fourier Transform.

@Yijun He Yes, but this is not what I meant.
As usual in mathematics we want to make our life easier, at least to start and generalize eventually. So, If we start with the quantum Fourier transform on 3 qubits for instance, to avoid a difficult and messy formalization at least at the beginning, then to what extent the nice applications of the quantum Fourier transform still make sense ?

view this post on Zulip Yijun He (Jul 26 2019 at 14:57):

I think quantum Fourier transform is just a faster way of computing the classical Fourier transform on qubits, so Shor's algorithm works (more slowly, but still correctly) even with the classical Fourier transform, and it doesn't depend on any nice property of the quantum one.

view this post on Zulip Anthony Bordg (Jul 26 2019 at 15:21):

I think quantum Fourier transform is just a faster way of computing the classical Fourier transform on qubits, so Shor's algorithm works (more slowly, but still correctly) even with the classical Fourier transform, and it doesn't depend on any nice property of the quantum one.

Yes, you're right and actually one could say the same thing about anything in quantum computing, it's "just" a way to speed up classical algorithms. But, the fast Fourier transform is already in the AFP and we want to contribute something new. Moreover, it would be a shame to lose your nice work on the quantum Fourier transform, but to avoid to get stuck we may need, at least temporarily, to assume a fixed number of qubits, then the formalization should be more workable.

view this post on Zulip Hanna Lachnitt (Aug 12 2019 at 09:01):

Hey :) I believe that I found a way to formalize quantum Fourier tranform without things getting so complicated in the first place. My controlled R gate is just a 4x4 matrix (as in the literature) and I use swapping to get the qubit needed in front of the unit vector (this seems to be done in practice as well). I am not entirely sure if this will avoid getting in trouble (it needs some unit vector decomposition lemmas) but I am pretty confident. @Yijun He do you feel this is a way I should pursue or do you think the current formalization is fixable? I will also have a more thoroughly look at the current file once I finish with Grover.

view this post on Zulip Yijun He (Aug 12 2019 at 10:40):

I still think the current proof is fixable, but a 4x4 controlled R gate sounds much better than the current proof. It would be great if you can help with the formalization of quantum Fourier transform.

view this post on Zulip Anthony Bordg (Aug 12 2019 at 15:17):

Hey :) I believe that I found a way to formalize quantum Fourier tranform without things getting so complicated in the first place. My controlled R gate is just a 4x4 matrix (as in the literature) and I use swapping to get the qubit needed in front of the unit vector (this seems to be done in practice as well).

@Hanna Lachnitt @Yijun He It sounds promising.

view this post on Zulip Hanna Lachnitt (Aug 16 2019 at 10:46):

Until now everything worked out, although of course there could be troubles later. I uploaded a first tentative theory in a QFT branch in my fork where I tried out my ideas. Everything is still under construction (especially some indices might be wrong). I hope I did not just do nonsense or made a stupid mistake :fear: However, I feel with this new approach proving becomes more difficult in terms of thinking about what parameters to use before proving something but the proofs themselves are rather easy now. And I feel that its well understandable for a reader especially with some explanations

view this post on Zulip Hanna Lachnitt (Aug 16 2019 at 10:50):

The idea behind the approach is not to define a matrix R_k with takes a huge unit vector and has to select all indices of qubits i and k to extend the binary fraction as this creates complexity. Instead swap the needed qubit jk|j_k\rangle outside of unit vector jl,...,jn| j_l,...,j_n \rangle (which is just a tensor product of single qubits, and jkj_k corresponds to the qubit at position k). Then, apply a 4x4 CR gate to the tensor product of this two qubits i and k. Since the second qubit is left untouched by this operation it can just be swapped back afterwards. This corresponds to an application of a RkR_k gate to qubit i.

view this post on Zulip Hanna Lachnitt (Aug 16 2019 at 10:54):

The file is still messy but I felt it was better to involve you in the process, I will make it more readable and add further proofs, so please pull from time to time if you have a look at it. Right now I am leaving proofs which are supposed to be very easy or bound to work for later to see if the overall approach is promising.

view this post on Zulip Hanna Lachnitt (Aug 30 2019 at 09:36):

Hey guys :) Just to keep you updated, I managed to prove calculation (5.4) from page 218 of Nielsen and Chuang. There are some easy proofs missing (including almost all gate proofs) but nothing that should cause any problems. The equivalence of (5.4) to the definition of quantum fourier transform is described as using only elementary algebra so I hope it will be doable :)

view this post on Zulip Hanna Lachnitt (Oct 19 2019 at 09:39):

@Anthony Bordg Regarding your comment about:
subsection ‹Transformation of j into a Tensor Product of Single Qubits›
what do you thing about:
subsection ‹Transformation of the Input into a Tensor Product of Single Qubits›

view this post on Zulip Anthony Bordg (Oct 19 2019 at 09:50):

Anthony Bordg Regarding your comment about:
subsection ‹Transformation of j into a Tensor Product of Single Qubits›
what do you thing about:
subsection ‹Transformation of the Input into a Tensor Product of Single Qubits›

@Hanna Lachnitt I think it's better. If I remember correctly "Mike and Ike", j|j\rangle is any basis state. Do you define qFt directly on an arbitrary state ? In other words is your "input" here refering to an arbitrary state ? If yes, why not simply "Transformation of a State into a Tensor Product of Single Qubits"? We could even later move this part into More_Tensor.thy.

view this post on Zulip Hanna Lachnitt (Oct 19 2019 at 18:18):

Yes qFt takes an arbitrary basis state (actually just a natural number). Sound good, I will take that. Especially if its moved to some other theory input does not make sense. Also I wrote an introductory comment which might explain things a bit better.

view this post on Zulip Hanna Lachnitt (Oct 19 2019 at 18:28):

As to your comment to to_list_bound:
Also, it seems that you start counting from 1 for the position s while all the rest of the library takes the convention that we start counting from 0.
I did this to stick closely to the literature where j1j2...jnj_1j_2...j_n are used for the binary representation of j. Actually I also did this for the CRiCR_i gates and so on. Otherwise it would be a bit confusing. While I work through the theory I will search for cases where I started to count from 0 it might be better to change them instead of changing the cases where counting starts from 1.

view this post on Zulip Hanna Lachnitt (Oct 19 2019 at 19:57):

I have renamed the abbreviation for to_tensor_prod j⨂ with ⨂r, standing for tensor product representation since j should not appear in any names

view this post on Zulip Hanna Lachnitt (Oct 20 2019 at 09:49):

Should the comments rather be texts?

view this post on Zulip Hanna Lachnitt (Oct 20 2019 at 10:09):

I decided to rename qr to phase_shifted_qubit, in short psq. I am still not 100% happy with that but qr is unacceptable. If there is a better possibility I would be happy for suggestions.

view this post on Zulip Hanna Lachnitt (Oct 20 2019 at 10:25):

Regarding your comment about lemma transpose_of_controlled_phase_shift: (* AB: Maybe simply transpose_of_CR ? *)
Isn't this the same thing as having H in a lemma name instead of hadamard_gate? So it would mix up notation and full name of the definition. But I would be happy to change this, shorter names would be preferable here.

view this post on Zulip Hanna Lachnitt (Oct 20 2019 at 13:20):

I also tried to change the definition qr/phase_shifted_qubit into an abbreviation. But then it got so slow that I had to set everything back. Might be just my laptop though, its not very powerful.

view this post on Zulip Anthony Bordg (Oct 21 2019 at 09:58):

Regarding your comment about lemma transpose_of_controlled_phase_shift: (* AB: Maybe simply transpose_of_CR ? *)
Isn't this the same thing as having H in a lemma name instead of hadamard_gate? So it would mix up notation and full name of the definition. But I would be happy to change this, shorter names would be preferable here.

There are two things we should absolutely avoid. First, variables in names. Second, notations in names if those notations are not standard. However, using very standard notations, like H or cR, in names is fine.

view this post on Zulip Hanna Lachnitt (Oct 21 2019 at 10:03):

Great, then I will change this, its much better readable.

view this post on Zulip Anthony Bordg (Oct 21 2019 at 10:30):

Should the comments rather be texts?

At some point we should replace the source comments with text blocks, but it's unimportant at that stage. They are more fundamental things we need first to take care

view this post on Zulip Hanna Lachnitt (Oct 21 2019 at 10:34):

Yes of course. I just replaced some of the latex code in the comments with the built-in code for readability, e.g. $|j_1,j_2,...,j_n\rangle$ with j1,j2,...,jn|j_1,j_2,...,j_n\rangle but if they are replaced with text at some point I would not do that.

view this post on Zulip Anthony Bordg (Oct 21 2019 at 10:46):

@Hanna Lachnitt There is something still confusing in the first comment. In your example, what's the link between j=11j=11 and 01011|01011\rangle ? Do you mean 00011|00011\rangle instead ?

view this post on Zulip Hanna Lachnitt (Oct 21 2019 at 11:06):

01011 is the binary representation of 11. I used the notation as it is introduced in the book of Nielsen and Chuang. To make it clearer I could add that j1j2...jn|j_1j_2...j_n\rangle = 01011|01011\rangle where j=j12n1+...+jn20j = j_1*2^{n-1}+...+j_n*2^0 which is simply written as j=j1...jnj=j_1...j_n in the book (the notation is a bit untidy).

view this post on Zulip Hanna Lachnitt (Oct 21 2019 at 11:10):

Indeed if one writes j|j\rangle what is meant is always j in binary representation (its really untidy), never something like 000j. Otherwise how would you encode e.g. 3 if 11 is 00011|00011\rangle?
I realize now that I maybe should take another number as example that does contain a digit beyond 1, e.g. 12. This might make it clearer and avoid confusion between binary and decimal representation.

view this post on Zulip Anthony Bordg (Oct 21 2019 at 11:21):

01011 is the binary representation of 11. I used the notation as it is introduced in the book of Nielsen and Chuang. To make it clearer I could add that j1j2...jn|j_1j_2...j_n\rangle = 01011|01011\rangle where j=j12n1+...+jn20j = j_1*2^{n-1}+...+j_n*2^0 which is simply written as j=j1...jnj=j_1...j_n in the book (the notation is a bit untidy).

Oh I see, it's eleven, not the binary representation 11 (namely 3)! Maybe it's better to use 9 or 12 to avoid any confusion.

view this post on Zulip Anthony Bordg (Oct 21 2019 at 11:37):

pow_tensor_list_one looks a bit cumbersome:

lemma pow_tensor_list_one [simp]:
  assumes "xs = []"
  shows "(pr (Cons x xs) 1) = x"
  by (simp add: assms)

It could simply be:

lemma pow_tensor_length_1:
  fixes X:: "complex Matrix.mat"
  shows "(pr [X] 1) = X"
  by simp

view this post on Zulip Anthony Bordg (Oct 21 2019 at 12:02):

@Hanna Lachnitt I made a new PR.

view this post on Zulip Hanna Lachnitt (Oct 23 2019 at 13:04):

Thanks for your PR, there seems to be still some confusion left about the binary representation. If j is a natural number strictly smaller than 2^m then the binary representation in this setting has length m, i.e. j=j1j2...jmj=j_1j_2...j_m and not length n.

I put m instead of n for some reasons (I used a locale in the first versions and needed another variable for inductions) but I wonder now if m should not be renamed to n since you would usually use j and n.

view this post on Zulip Hanna Lachnitt (Oct 23 2019 at 13:08):

pow_tensor_list_one looks a bit cumbersome:

Thanks! I only used Cons because of our talk about when to use (Suc n) instead of (n+1) and this is not a lemma that is for people to look at it. I removed the type annotation (fixes X:: "complex Matrix.mat") however, since it was done nowhere else.

view this post on Zulip Hanna Lachnitt (Oct 23 2019 at 13:10):

double post

view this post on Zulip Anthony Bordg (Oct 23 2019 at 15:44):

pow_tensor_list_one looks a bit cumbersome:

Thanks! I only used Cons because of our talk about when to use (Suc n) instead of (n+1) and this is not a lemma that is for people to look at it. I removed the type annotation (fixes X:: "complex Matrix.mat") however, since it was done nowhere else.

Formal proofs is a tricky business. A rule has exceptions, but there is the spirit of the rule. Regarding canonical forms, sometimes they will help, in particular in involved proofs, but here the proof is trivial. So, here canonical forms only make the statement less legible.

view this post on Zulip Anthony Bordg (Oct 28 2019 at 11:13):

I put m instead of n for some reasons (I used a locale in the first versions and needed another variable for inductions) but I wonder now if m should not be renamed to n since you would usually use j and n.

Yes, it would be better to use n for the number of qubits to be consistent across the library. To be consistent would help the readers and the maintainers.
Also, why use the variable k to denote a length when one can use l ?

view this post on Zulip Hanna Lachnitt (Oct 28 2019 at 20:21):

On another issue, should j also be replaced by j_dec or jd? Otherwise it is a bit cumbersome if j appears inside of a matrix, e.g.
(Matrix.mat 2 1 (λ(i,j). if i=0 then (1::complex)/sqrt(2) else (exp (complex_of_real (2*pi)*𝗂*(bin_frac (s-1) (t-1) n jd)))*1/sqrt(2)))"

view this post on Zulip Hanna Lachnitt (Oct 28 2019 at 20:24):

I am currently working towards replacing m by n and k with l if its used for a length


Last updated: Sep 25 2022 at 23:25 UTC