Zulip Chat Archive

Stream: new members

Topic: Using data.rat


view this post on Zulip Bhavik Mehta (Nov 16 2019 at 21:54):

I'm struggling with proving basic things for rational numbers - could anyone provide some hints for this problem?

example {a b n : } {h : n  0} : rat.mk a b / n = rat.mk a (b * n) := sorry

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:02):

I can't find anything useful in data.rat.basic

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 22:02):

Yeah, similarly

view this post on Zulip Reid Barton (Nov 16 2019 at 22:07):

rat.mk a b equals (\u a) / (\u b) right? (\u being the up arrow)

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 22:07):

I think I've got the skeleton of the proof, with some (I think easy) technicalities missing:

example {a b n : } {h : n  0} : rat.mk a b / n = rat.mk a (b * n) :=
begin
  suffices : rat.mk a b = rat.mk a (b * n) * n,
    rw this, rw mul_div_cancel, sorry,
  rw [rat.coe_nat_eq_mk, rat.mul_def, mul_one, rat.div_mk_div_cancel_left], sorry
end

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 22:10):

rat.mk a b equals (\u a) / (\u b) right? (\u being the up arrow)

Yeah, if the \u are casting correctly to Q

view this post on Zulip Reid Barton (Nov 16 2019 at 22:13):

If you rewrite with that first, then it should be a general div_mul or something

view this post on Zulip Reid Barton (Nov 16 2019 at 22:13):

Well, after more facts about casts I guess...

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 22:20):

rw [rat.mk_eq_div, rat.mk_eq_div], simp, rw div_div_eq_div_mul does it, thanks!

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:23):

Is the idea that you're not supposed to be using rat.mk?

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:25):

BTW, is there any good reason not to define structures on data.rat by equiv.discrete_field (_ : equiv data.rat (fraction_field int))? Won't we get many theorems for free in this case?

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 22:26):

data.rat says: "It is defined as the set of pairs ⟨n, d⟩ of integers such that d is positive and n and d are coprime. This representation is preferred to the quotient because without periodic reduction, the numerator and denominator can grow exponentially (for example, adding 1/2 to itself repeatedly)."

view this post on Zulip Chris Hughes (Nov 16 2019 at 22:26):

The best solution is to use division and not rat.mk

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:26):

Coerce everything to Q first?

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:27):

@Bhavik Mehta I was talking about operations on rat and theorems about these operations, not the data type.

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 22:28):

@Yury G. Kudryashov Ah okay, my mistake

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:29):

Most operations (except for neg?) need "cancel numerator and denominator" step anyway.

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:29):

And this is exactly what functions from equiv/algebra will do.

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 22:55):

The best solution is to use division and not rat.mk

This is so much less painful, thanks!!

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:56):

I think the way it works is that there's a "mathlib standard way" to do things, and you have to learn it for the things you want to do.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:56):

Often you can learn it by simply reading the relevant mathlib files.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 22:57):

rat.mk is indeed supposed to be internal to the data.rat file and not used once \u a / \u b works

view this post on Zulip Mario Carneiro (Nov 16 2019 at 22:58):

unless you care about computation and need a more efficient way of building the number

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 23:00):

Is there some general way of finding out this sort of thing? Reading the mathlib files around data/rat seemed to mostly use rat.mk

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:01):

I suspect that Chris has used rat sufficiently often to know the tricks. Should his observation be made in the module docstring?

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 23:01):

I'd certainly have appreciated that

view this post on Zulip Chris Hughes (Nov 16 2019 at 23:01):

I think it probably should since it's something I've seen a few people do.

view this post on Zulip Chris Hughes (Nov 16 2019 at 23:02):

Maybe a docstring on rat.mk as well.

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 23:02):

Tangentially related, I've now got my goal in a slightly nicer form, but there's \us around - I can't tell if they're casting my nats up to ints or to Q, is there some way I could find out?

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:03):

I can't help but thinking that it shouldn't matter nowadays, because of all the cast tactics. One answer to your question is to write set_option pp.all true above your work.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:04):

There might be a less drastic way to do it. This way tells you exactly which term you're looking at.

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 23:04):

Yikes, that's far harder to parse

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 23:05):

Wait - cast tactics

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:05):

If you post fully working code I can try and make sense of the pp.all output if you want

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:06):

norm_cast and friends should I think sort out problems with casts from nat to int to rat nowadays.

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 23:06):

I didn't know cast tactics were a thing! norm_cast managed perfectly

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:08):

You are trying to do mathematics in Lean and you are running into exactly the problems which me and my students started running into two years ago, but you have the advantage that some of our problems were solved by computer scientists in the mean time.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:08):

This is why I have so much hope in this software.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:08):

When I came here I asked how to prove 2+2=42+2=4 and they said "which 2?" and I said "the real number 2" and they said "oh boy that's hard"

view this post on Zulip Bhavik Mehta (Nov 16 2019 at 23:09):

That's good to hear - I think I'd still like some documentation for this sort of thing

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:09):

When Chris came here he asked how to prove (x+y)3=x3+3x2y+3xy2+y3(x+y)^3=x^3+3x^2y+3xy^2+y^3 and they said "oh boy that's hard"

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:10):

but then people like Rob and Mario and people supervised by them pop out of the woodwork and write tactics which solve these things.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:23):

to clarify, 2 + 2 = 4 is not hard at all, but it is hard to "do it without doing it" because that's asking to have a general procedure

view this post on Zulip Chris Hughes (Nov 16 2019 at 23:23):

example {α : Type*} [has_one α] [has_add α] : (2 : α) + 2 = 4 := rfl

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:24):

I think the precise example was (1 : real) \ne 2

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:24):

and there was no norm_num at the time

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:24):

and the other one was (2 : real)^2 - 3 * 2 + 2 = 0

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:25):

it's still easy, it's just that you get upset when I tell you that the answer is to reduce 1 != 2 to 1 < 2 and then 0 < 1 and finish

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:25):

2 years ago this was harder for a newbie, that's all I'm saying.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:25):

you don't want that proof

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:26):

I want that 1 : real and 2 : real are not equal by schoolkid, because any schoolkid knows it.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:26):

And we now have that with norm_num

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:26):

exactly, you want a proof which doesn't look like a proof

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:26):

Right. It's obvious so it doesn't need a proof.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:26):

that's false

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:26):

Not to a mathematician.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:26):

but you want a tactic to pretend it is true

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:27):

Right. I want to speak to Lean like a mathematician.

view this post on Zulip Chris Hughes (Nov 16 2019 at 23:27):

it's still easy, it's just that you get upset when I tell you that the answer is to reduce 1 != 2 to 1 < 2 and then 0 < 1 and finish

Can you do this example : (1 : ℂ) ≠ 2 :=? You're even allowed to use norm_num if you want.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:27):

Why do you think I sunk several hours this evening into making X + Y make sense for X Y : set real?

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:28):

In that case, I would either reduce to 0 != 1, or for larger numbers I would interpret them in real or nat and then use <

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:28):

This (X + Y) is something which doesn't even need a definition for mathematicians, they will expect to be able to sum subsets of the reals, but we can't do it in mathlib yet.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:28):

We can do it, but the notation is funky

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:29):

it is (+) <$> X <*> Y

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:29):

Yeah well not only do I want X + Y to work, but I want X + (Y + Z) to be provably X + Y + Z by undergraduate.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:30):

There is also the issue that this notation is very general and overloaded in maths

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:31):

sure but the notation here is reasonable. It's standard in maths to add two subsets of the reals when you're teaching sups.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:31):

you also have things like A + a and B - A (and -A is already being used for complement)

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:31):

Yes sure, we do that too, but I'm not asking for that yet :D

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:32):

I'm just asking for X+Y which I don't think is unreasonable. Do you have a problem with the PR or are you just observing that I won't be able to get much further?

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:32):

I would suggest you not pretend this is actually addition of sets

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:32):

use another notation

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:32):

But you're happy to have X * Y for X Y : set M with monoid M?

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:33):

I think it's probably a bad idea, because it will beg the question

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:33):

But this is already in mathlib.

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:33):

probably a sneak attack

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:34):

I'm happy to make the additive version local notation, I definitely want it in the real number game

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:34):

https://github.com/leanprover-community/mathlib/blob/61ccaf65c4cfc9c6ff103463342e034347eb8b89/src/algebra/pointwise.lean#L27

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:34):

https://github.com/leanprover-community/mathlib/blob/61ccaf65c4cfc9c6ff103463342e034347eb8b89/src/algebra/pointwise.lean#L65

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:35):

I note that they're not instances.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:35):

How about I make them defs?

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:37):

I mean https://github.com/leanprover-community/mathlib/blob/a9a8e6975cf8b7c9b75edb0231c207ae5f2b9a17/src/algebra/pointwise.lean#L188 and https://github.com/leanprover-community/mathlib/blob/a9a8e6975cf8b7c9b75edb0231c207ae5f2b9a17/src/algebra/pointwise.lean#L191 (change from instance to def)

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:38):

Oh, I see I was involved in merging #854 and I think the reason was because it didn't make them instances

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:39):

If it's just a def, then it's just a theory about these operations and this is certainly useful

view this post on Zulip Mario Carneiro (Nov 16 2019 at 23:39):

make it a local instance and you should be golden

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 01:11):

it is (+) <$> X <*> Y

If Hales had his controlled natural language, could he have X+YX+Y meaning this? I have realised that sometimes one can use the CNL instead of notation.

view this post on Zulip Mario Carneiro (Nov 17 2019 at 01:12):

anything is possible

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 01:13):

My understanding is that he wants a language which is readable both by humans and by Lean.

view this post on Zulip Mario Carneiro (Nov 17 2019 at 01:14):

the translator might become unbounded in complexity, but it's not exactly an unsolvable problem from the CS point of view

view this post on Zulip Mario Carneiro (Nov 17 2019 at 01:14):

it's just that once you pin down an actual notation system, certain things become more difficult or impossible because the limitations are explicit

view this post on Zulip Mario Carneiro (Nov 17 2019 at 01:16):

If you are okay with a behemoth of a notation parser, then anything is possible, but it makes it harder for the user to predict what things mean if the parser isn't perfect, fails on some input, or gives a wrong result

view this post on Zulip Mario Carneiro (Nov 17 2019 at 01:19):

I recall seeing snippets of Hales's CNL and if I understand correctly the proposed solution is to have an unambiguous notation system (in the form of a bunch of tex macros) which "decays" to lean notation and also to latex notation, and I see no problem with this except that I thought that mathematicians can't tolerate unambiguous notation. If putting things in the latex context helps mathematicians get over this mental hurdle then I'm all for it

view this post on Zulip Reid Barton (Nov 17 2019 at 01:48):

I would have said mathematical notation is often ambiguous. I guess whether or not something is ambiguous depends on how much of the context you consider. This ability isn't even just about being a human, it depends on knowing which of the possible interpretations is plausible, and consistent with the surrounding arguments, etc.

view this post on Zulip Reid Barton (Nov 17 2019 at 01:50):

As a lame example, I'm always going to guess sin2x\sin^2 x means (sinx)2(\sin x)^2 because there's no plausible reason to ever have sin(sinx)\sin(\sin x), and then if in the next line it is replaced by 1cos2x1 - \cos^2 x, then I'm even more certain.

view this post on Zulip Reid Barton (Nov 17 2019 at 01:57):

However you end up doing it, it seems reasonable to give the machine something more specific but present an abbreviated, ambiguous form to the human reader

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:01):

Norm Megill, the author of metamath, has some strong opinions on this which I partly agree with. Even if notations are unambiguous in the computer, if they are ambiguated during printing, then it is easy to create misleading statements. This is what "Pollack consistency" is all about. I don't like the idea that the statement of a theorem should not be understandable without its proof, but I very commonly have to deal with this when reading actual maths papers

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:04):

When I started using Lean I was really all for mathematical imprecision to be possible, like f(X)f(X) just meaning {f(x):xX}\{f(x):x\in X\}.

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:05):

In some ways it makes sense: as a method of human communication, we often use the "principle of charity", where we take the most lenient possible understanding in order to justify an argument, and sometimes this can be taken to extremes in maths where you have folks like Mochizuki who produce something that clearly fails to communicate but the maths community is only willing to say "we aren't sure if this is correct" even after years of analysis rather than "this is nonsense" like a formal theorem prover would do

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:07):

But the more I use it the more I realise that actually I think we should start to think as mathematicans about firstly forcing ourselves to distinguish between these closely-related (for us) notions and secondly about formalising exactly the notation-cheats which we are prepared to tolerate. If one mathematician is genuinely using a piece of notation to mean one thing in dependent type theory, and another mathematician is using the same piece of notation to mean a different thing, then that should be OK, as long as each mathematician is consistent. That's what we want from our notation.

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:10):

I think even this, the CS people are happy to tolerate, provided the different notations go in different namespaces or some similar broad scoping. But then they say "but you promise not to use these at the same time, right?" and you say "uhh...". Of course some enterprising mathematician is later going to want to work in both fields, and use both conflicting notations, maybe apologize but use them anyway, and now the CS person is scratching their head trying to figure out what means what when and how you can possibly tell

view this post on Zulip Reid Barton (Nov 17 2019 at 02:15):

Well we don't really know how we can tell either, but it's easy

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:17):

humans have the advantage here, because they can "cross that bridge when they come to it", give it a bit of thought, and maybe change the game if it's too hard (by changing notations later)

view this post on Zulip Reid Barton (Nov 17 2019 at 02:21):

How do we tell whether \otimes is the tensor product of modules, the tensor product of elements or the tensor product of maps? It's hard to imagine being confused about this--provided you understand roughly what is going on.

view this post on Zulip Reid Barton (Nov 17 2019 at 02:21):

Maybe Lean 3 can just about do this, with overloaded notations

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:33):

@Patrick Massot found a very subtle notational instance in Bourbaki where I think the completion notation was being used in some very subtle ways.

view this post on Zulip Reid Barton (Nov 17 2019 at 02:34):

Perhaps it's not the case for metamath, but Lean already does a lot of context-sensitive elaboration anyways, so I'm not sure you lose much by erasing more distinctions.

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:37):

in metamath we use only global notations, with variables acting as local notations when needed

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:38):

as I said, Norm definitely doesn't want "hidden magic" and all metamath terms are basically pp.all

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:39):

I think it's impressive how close metamath gets to a passable mathematical notation with zero implicit arguments and no type inference

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:40):

Why don't you make type inference for metamath using prolog?

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:41):

that would be an interesting project

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:41):

I mean metamath the language doesn't have type inference

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:41):

the IDEs have a couple things that get close to type inference

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:42):

Gotcha. Do the IDE's use prolog or do they roll their own -- didn't Leo roll his own?

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:42):

And they're rolling out a completely new one for Lean 4 I guess.

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:43):

I wrote a "prolog-like search" but it doesn't do any backtracking, so it only uses lemmas that are always useful to apply when applicable

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:43):

there isn't much distinction made between goals that are about typing and goals that are theorems

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:44):

of course, the whole point of DTT is that the distinction is fuzzy

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:45):

Can you say that thing about goals within type theory? By a goal do you mean a proposition or a proof?

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:45):

a metavariable standing for a proof of a known expression

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:46):

i.e. what the tactic state normally calls a goal

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:46):

Are you talking about expr?

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:46):

I don't know anything about how the tactic state works.

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:46):

All I know is that it's a much better fit for my brain than term mode

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:46):

you have a hole where a proof is expected, and you refine that hole with a partial proof

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 02:47):

right

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:47):

sure, that's how almost every theorem prover works

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:48):

But in programming languages, where it is an outgrowth of term construction, you work from the bottom up, inferring types of known expressions rather than refining unknown proofs of known types

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:51):

There was once a tactic called back that I thought was going to land in mathlib, not sure what happened to it. The tactic I wrote for metamath was basically that, and it allowed you to discharge a variety of problems like equality proofs (rewrite), closure proofs (typing), and other limited decision procedures similar to type class inference like continuity inference

view this post on Zulip Mario Carneiro (Nov 17 2019 at 02:53):

Interestingly, continuity inference in metamath is possible by a matching based method that doesn't work in lean because of the way lambdas are handled in type theory

view this post on Zulip Johan Commelin (Nov 18 2019 at 08:38):

@Scott Morrison Hi! People are talking about back. How are things going? :wink:

view this post on Zulip Johan Commelin (Nov 18 2019 at 08:40):

@Mario Carneiro I've made several serious attempts at parsing metamath statements in that web-rendered version of set.mm. I've always failed miserably. I really can't read mm at the moment. There is quite a gap to bridge. With lean I had no such issue at all.

view this post on Zulip Mario Carneiro (Nov 18 2019 at 08:42):

In the corner of every metamath page, there is a "structured version" button, that is trying out an experimental rendering method using mathjax instead of unicode. Does that help at all? We are of course always looking for ways to increase readability

view this post on Zulip Johan Commelin (Nov 18 2019 at 08:43):

What is a good example...

view this post on Zulip Johan Commelin (Nov 18 2019 at 08:43):

Let me see if I can parse PNT

view this post on Zulip Johan Commelin (Nov 18 2019 at 08:46):

I end up on a page like this: http://us.metamath.org/mpeuni/mudivsum.html and nothing feels familiar...

view this post on Zulip Johan Commelin (Nov 18 2019 at 08:46):

I don't know how to pronounce mpeuni. I can make a guess for mudivsum

view this post on Zulip Mario Carneiro (Nov 18 2019 at 08:47):

it stands for metamath proof explorer, unicode version

view this post on Zulip Mario Carneiro (Nov 18 2019 at 08:48):

mudivsum says that nxμ(n)n=O(1)\sum_{n\le x}\frac{\mu(n)}n=O(1)

view this post on Zulip Mario Carneiro (Nov 18 2019 at 08:48):

where μ\mu is the number-theoretic Mobius function

view this post on Zulip Mario Carneiro (Nov 18 2019 at 08:49):

If you wanted to know what "sum", "mu", or "O(1)" mean in that statement, you can find them in the "syntax hints" at the bottom of the page

view this post on Zulip Johan Commelin (Nov 18 2019 at 08:51):

Aha, I see


Last updated: May 09 2021 at 23:10 UTC