## Stream: maths

### Topic: Perfect Numbers

#### Aaron Anderson (Jun 17 2020 at 03:30):

I have a rough but working proof of the Perfect Number/Euclid-Euler Theorem, Freek 70, at https://github.com/awainverse/perfect_number

#### Aaron Anderson (Jun 17 2020 at 03:31):

I’m interested in people’s input on several things. One thing that comes to mind is whether some of the nat variables should be replaced with pnats.

#### Johan Commelin (Jun 17 2020 at 05:05):

@Aaron Anderson Interesting! I will write some feedback after breakfast.

#### Yury G. Kudryashov (Jun 17 2020 at 05:07):

If it builds, then we can add it to our list.

#### Yury G. Kudryashov (Jun 17 2020 at 05:09):

Could you please open a PR to mathlib/archive? We'll probably want to merge some parts to src/ but it would be nice to have a green light from CI before adding a link to this PR to the website.

#### Aaron Anderson (Jun 17 2020 at 05:56):

I'm trying to figure out how, but creating my own repository to host this today was already stretching my understanding of github...

#### Bryan Gin-ge Chen (Jun 17 2020 at 05:58):

I just downloaded the repo and it built locally with no warnings or errors.

#### Johan Commelin (Jun 17 2020 at 06:02):

@Aaron Anderson We can coach you through it.

#### Johan Commelin (Jun 17 2020 at 06:03):

Are you on windows or linux?

(Or mac...)

Linux.

#### Johan Commelin (Jun 17 2020 at 06:04):

Ooh great, than it's easy-peasy

#### Aaron Anderson (Jun 17 2020 at 06:05):

I know a few of the basic git commands at this point

#### Johan Commelin (Jun 17 2020 at 06:05):

Do you by chance have leanproject installed?

#### Aaron Anderson (Jun 17 2020 at 06:05):

Yes, and I used that to create my perfect_number repo

Ok, great.

#### Aaron Anderson (Jun 17 2020 at 06:08):

(I've accepted the email invitation)

#### Johan Commelin (Jun 17 2020 at 06:09):

@Aaron Anderson so if you accept that invitation, and then leanproject get mathlib (in a directory where you do not yet have a copy of mathlib), then you are halfway there.

#### Aaron Anderson (Jun 17 2020 at 06:12):

Ok, I've done that, and have a "mathlib" folder on my computer.

#### Johan Commelin (Jun 17 2020 at 06:12):

After that, you can write

git checkout -b freek-70


#### Johan Commelin (Jun 17 2020 at 06:12):

This creates a new branch, for your PR

#### Johan Commelin (Jun 17 2020 at 06:13):

After that, you have to copy your file to
archive/100-theorems-list/70_perfect_numbers.lean

#### Johan Commelin (Jun 17 2020 at 06:13):

(Or something like that)

#### Johan Commelin (Jun 17 2020 at 06:13):

And then

git add archive/100-theorems-list/70_perfect_numbers.lean
git commit


#### Johan Commelin (Jun 17 2020 at 06:14):

In the commit message, you can use something like

feat(archive/100-theorems-list): perfect numbers (nr 70)


or something better (-;

#### Johan Commelin (Jun 17 2020 at 06:15):

Once you have done that:

git push


and this will give an error message, saying that you need to set an upstream thingy. It will tell you which command to execute instead. Do that.

#### Johan Commelin (Jun 17 2020 at 06:16):

This last command will give you a URL in it's output. You can visit that URL to open a PR.
(Alternatively, just go to the mathlib page on github, and it will recognise that you recently pushed a branch, and suggest to open a PR.)

#### Johan Commelin (Jun 17 2020 at 06:17):

Finally, you can (if you want :stuck_out_tongue_wink:) post a message here of the form #3057 where 3057 is the PR number on the github page, and Zulip will automatically turn it into a link that we can click on to see your latest creation.

#### Johan Commelin (Jun 17 2020 at 06:22):

Now for some feedback on the code. I've gone through the first 100 lines or so.

import data.nat.totient

open_locale classical
open_locale big_operators

section definitions

variable (n : ℕ)

def divisors : finset ℕ :=
finset.filter (λ x : ℕ, x ∣ n) (finset.Ico 1 (n + 1))

def proper_divisors : finset ℕ :=
finset.filter (λ x : ℕ, x ∣ n) (finset.Ico 1 n)

lemma not_proper_self :
n ∉ proper_divisors n :=
by simp [proper_divisors]

lemma mem_divisors {m : ℕ} :
n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0:=
begin
suffices : n ∣ m ∧ 1 ≤ n ∧ n < m + 1 ↔ n ∣ m ∧ ¬m = 0,
by simpa only [divisors, finset.Ico.mem, ne.def, finset.mem_filter, and_comm],
split,
{ intro hyp, refine ⟨hyp.left, _⟩, have h1 := hyp.right, omega },
{ intro hyp, refine ⟨hyp.left, _⟩,
rcases hyp with ⟨⟨c, rfl⟩, nonzero⟩,
split,
{ cases n,
{ simpa using nonzero },
{ exact nat.le_add_left _ _, }, },
{ cases c,
{ simpa using nonzero },
{ calc n = n * 1           : by rw mul_one
... ≤ n * (c + 1)     : nat.mul_le_mul_left _ (nat.le_add_left _ _)
... < n * (c + 1) + 1 : nat.lt_succ_self _, } } }
end

variable {n}

lemma le_of_mem_divisors {m : ℕ} (h : n ∈ divisors m) : n ≤ m :=
by { rw [mem_divisors, ← nat.pos_iff_ne_zero] at h, apply nat.le_of_dvd h.2 h.1 }

variable (n)

--lemma mem_proper_divisors : sorry := sorry

lemma divisors_eq_proper_divisors_insert_self (posn : 0 < n) :
divisors n = insert n (proper_divisors n) :=
begin
ext,
simp only [finset.mem_insert, divisors, proper_divisors, finset.Ico.succ_top posn,
finset.filter_insert, if_true, dvd_refl, finset.mem_insert],
end

def sum_divisors : ℕ :=
∑ i in divisors n, i

def sum_proper_divisors : ℕ :=
∑ i in proper_divisors n, i

@[simp] lemma divisors_zero : divisors 0 = ∅ := dec_trivial

@[simp] lemma proper_divisors_zero : proper_divisors 0 = ∅ := dec_trivial

@[simp] lemma sum_divisors_zero : sum_divisors 0 = 0 := dec_trivial

@[simp] lemma sum_proper_divisors_zero : sum_proper_divisors 0 = 0 := dec_trivial

sum_divisors n = sum_proper_divisors n + n :=
begin
by_cases h : n = 0, { simp [h] },
replace h : 0 < n := nat.pos_iff_ne_zero.mpr h,
rw [sum_divisors, sum_proper_divisors, divisors_eq_proper_divisors_insert_self _ h,
end

def perfect : Prop :=
sum_proper_divisors n = n

end definitions

section basic_lemmas

lemma perfect_iff_sum_divisors_twice {n : ℕ} :
perfect n ↔ sum_divisors n = 2 * n :=
by { rw [sum_divisors_eq_sum_proper_divisors_add_self, perfect], omega }

@[simp] lemma divisors_one : divisors 1 = ({1} : finset ℕ) :=
by { ext, rw mem_divisors, simp }

lemma one_mem_divisors {n : ℕ} (nonzero : n ≠ 0):
1 ∈ divisors n :=
by simp [mem_divisors, nonzero]

lemma self_mem_divisors {n : ℕ} (nonzero : n ≠ 0):
n ∈ divisors n :=
by simp [mem_divisors, nonzero]

lemma pos_sum_divisors {n : ℕ} (posn : 0 < n) :
0 < sum_divisors n :=
begin
rw nat.pos_iff_ne_zero at posn,
calc 0 = ∑ i in divisors n, 0 : finset.sum_const_zero.symm
... < sum_divisors n       : finset.sum_lt_sum (λ _ _, nat.zero_le _) _,
use 1, exact ⟨one_mem_divisors posn, nat.zero_lt_one⟩,
end


#3094

#### Johan Commelin (Jun 17 2020 at 06:22):

I should say that I think the code was already really good!

#### Johan Commelin (Jun 17 2020 at 06:23):

@Aaron Anderson Nice!

#### Johan Commelin (Jun 17 2020 at 06:24):

Another thing that can make your life easier: you often need to exclude n = 0. Sometimes you use 0 < n, sometimes 0 ≠ n. You should choose one, and use it everywhere. It will make it a lot easier to pass the assumption back and forth.
Now you constantly need to convert between the two versions.

#### Aaron Anderson (Jun 17 2020 at 06:25):

I'm still wondering if I do anything that'd make it difficult to just shift to pnats

#### Johan Commelin (Jun 17 2020 at 06:26):

It might help a bit... But I'm not sure if it will matter much

#### Kevin Buzzard (Jun 17 2020 at 06:27):

I think the correct thing to say here is "sure, just switch to pnats, and when you find holes in the pnat library just make a PR to mathlib which fixes them"

#### Johan Commelin (Jun 17 2020 at 06:27):

Another thing:

src/number_theory/lucas_lehmer.lean:def mersenne (p : ℕ) : ℕ := 2^p - 1


#### Johan Commelin (Jun 17 2020 at 06:27):

You could import that file.

#### Johan Commelin (Jun 17 2020 at 06:27):

Maybe it even contains some lemmas that you could reuse.

#### Kevin Buzzard (Jun 17 2020 at 06:27):

I think pnats deserve some more love

#### Johan Commelin (Jun 17 2020 at 06:29):

@Aaron Anderson and there is also

src/data/padics/padic_norm.lean:def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=


which can help with the multiplicity lemmas

#### Johan Commelin (Jun 17 2020 at 06:33):

@Yury G. Kudryashov Don't you think that 95% of the code should go into src/?

#### Johan Commelin (Jun 17 2020 at 06:34):

@Aaron Anderson A lot of your lemmas seem useful and reusable. So we might want to butcher your file into tiny pieces that end up in 10 different places in mathlib.

Awesome.

#### Aaron Anderson (Jun 17 2020 at 06:35):

I think pnats might be good for defining multiplicative functions in general

#### Johan Commelin (Jun 17 2020 at 06:36):

Feel free to experiment!

#### Johan Commelin (Jun 17 2020 at 07:04):

@Aaron Anderson By the way, probably relevant: if you want to make changes to the code in the PR, just edit the files in your clone of mathlib, and then git commit -a, write a message, and git push. That's it.

#### Kenny Lau (Jun 17 2020 at 07:23):

I use git commit -am "message"

#### Patrick Massot (Jun 17 2020 at 07:36):

Johan, if you don't have a convenient link you could have used instead of writing all those git explanations then you're welcome to copy paste this into our contributing guide, or a new file linked from our contributing guide.

#### Yury G. Kudryashov (Jun 17 2020 at 07:43):

Johan Commelin said:

Yury G. Kudryashov Don't you think that 95% of the code should go into src/?

I didn't look at the code yet.

#### Aaron Anderson (Jun 18 2020 at 06:13):

I've started refactoring to pnats. Proving inequalities is easier, but the tactics seem much weaker. Along the way, I found that having to switch between pnats and nats made me want to use nat.primes for my prime numbers, but this is maybe too cumbersome...

#### Aaron Anderson (Jun 18 2020 at 06:13):

It's in a new file here https://github.com/awainverse/perfect_number

#### Aaron Anderson (Jun 18 2020 at 06:17):

I'd like to be able to talk about multiplicative functions in general, and prove something to the effect of ∀ n : ℕ+, f(n) = (factorisation n).prod (λ p : nat.primes, λ k : ℕ, f (p ^ k)) for a multiplicative function f, and factorisation a finsupp of multiplicities

#### Aaron Anderson (Jun 18 2020 at 06:18):

I think this is a good argument that I should keep going on pnats, and maybe nat.primes?

#### Kevin Buzzard (Jun 18 2020 at 06:31):

The reason I would not use pnats if I were knocking off this sort of proof is precisely that they're not as well developed as nats, and the reason they're not as well developed is precisely because people don't use them. This vicious circle is not there for any particular reason and that's why I think keeping going on pnats is a good idea. Any factoring stuff will work better with pnats than nats the moment pnats have the right infrastructure. Pnats are a monoid with cancellation; monoids with 0 are a different thing somehow

#### Aaron Anderson (Jun 18 2020 at 17:45):

Well, I have no idea how the omega tactic works, other than sometimes it solves my problems with nats, but as I go I'm designating which lemmas about pnats maybe should be simp lemmas

#### Aaron Anderson (Jun 20 2020 at 01:09):

I'm proving (usually 2-line proofs or so) a lot of lemmas about pnats which are basically wrappers for existing nat lemmas. I think pnats would be way more useful if there was a common generalization of some kind of divisibility-structure, and facts about coprime and gcd were proved for that.

#### Aaron Anderson (Jun 20 2020 at 01:10):

I know that ring_theory/coprime exists, but pnats aren't a semiring, and gcd doesn't seem to be defined in that context.

#### Aaron Anderson (Jun 20 2020 at 01:11):

This probably wants some definition of a divisibilty poset?

#### Aaron Anderson (Jun 20 2020 at 01:12):

(Not at all necessary just to get this project in mathlib, but it'd be cool to start proving things about multiplicative functions, Dirichlet convolution, and even incidence algebras)

#### Johan Commelin (Jun 20 2020 at 05:05):

@Aaron Anderson Do you have any idea what kind of structure you need (weaker than semiring) in which you can prove your facts?

#### Johan Commelin (Jun 20 2020 at 05:07):

I guess (tongue in cheek) you might need a canonically_ordered_semirig

#### Aaron Anderson (Jun 20 2020 at 05:18):

I think that addition is unnecessary, a comm_monoid should be enough context

#### Aaron Anderson (Jun 20 2020 at 05:21):

Or perhaps has_dvd

#### Bryan Gin-ge Chen (Jun 20 2020 at 05:21):

Incidence algebras would be great!

#### Aaron Anderson (Jun 20 2020 at 05:22):

Something like “if you have an operation called gcd, which is provably equivalent to the sup in the poset with relation dvd, which has sensible properties, then you have these lemmas”

#### Alex J. Best (Jun 20 2020 at 05:26):

I did a tiny bit on incidence algebras a long time ago, its completely broken now :sad: (but I guess this means mathlib has advanced a lot) (and it was badly written / experimental to begin with) but just in case you are curious here is what I had:

import tactic
import data.rat.basic
import data.set.intervals
import data.set.finite
import init.algebra.order

open nat set

variable (α : Type*)

class locally_finite extends partial_order α :=
(fin_Icc : ∀ x y : α, fintype (Icc x y))

def my_Icc (n m : ℕ) : list ℕ := list.range' n (m - n + 1)
def Icc_multi (n m : ℕ) : multiset ℕ := my_Icc n m
theorem nodup (n m : ℕ) : list.nodup (my_Icc n m) :=
by dsimp [my_Icc]; simp [list.nodup_range']

theorem my_nodup (n m : ℕ) : multiset.nodup (Icc_multi n m) := nodup _ _
def tIcc (n m : ℕ) : finset ℕ := ⟨_, my_nodup n m⟩

instance Icc_ℕ_fintype (l u : ℕ) : fintype (Icc l u) :=
fintype.of_finset (tIcc l u) (λ x,
begin split, intro h,simp [h], split, {simp [(∈)] at h, sorry},sorry,sorry, end)

instance : partial_order ℕ := by apply_instance

instance : locally_finite ℕ :=
{ fin_Icc := λ x y, Icc_ℕ_fintype x y,
..nat.partial_order }

variables [locally_finite α] (R : Type*) [comm_ring R]

def incidence_algebra := α → α → R

def δ [decidable_eq α] : incidence_algebra α R :=
λ x y, if x = y then 1 else 0

#check δ ℕ ℤ
#eval δ ℕ ℤ 1 0

def ζ [@decidable_rel α (≤)] : incidence_algebra α R :=
λ x y, if x ≤ y then 1 else 0

#check ζ ℕ ℤ
#eval ζ ℕ ℤ 1 3
#eval ζ ℕ ℤ 1 0

instance [decidable_eq α] : has_one (incidence_algebra α R) := ⟨δ α R⟩

instance : has_mul (incidence_algebra α R) :=
⟨λ f g x y, finset.sum ((locally_finite.fin_Icc x y).elems) (λ z, f x z * g z y)⟩

#check (δ ℕ ℤ * δ ℕ ℤ)
#eval (δ ℕ ℤ * δ ℕ ℤ) 1 1
#eval (δ ℕ ℤ * ζ ℕ ℤ) 1 1

instance [decidable_eq α] : monoid (incidence_algebra α R) :=
{ mul := (*),
mul_assoc := λ x y z, begin sorry end,
one := (1),
one_mul := λ a, begin ext x y, simp [(*),has_one.one,δ],sorry end,
mul_one := sorry }

instance (x y : α) : fintype (Icc x y) := locally_finite.fin_Icc x y

lemma card_Icc_lt_card_Icc_of_lt (x y z : α) (hxz : x ≤ z) (hzy : z < y) : fintype.card (Icc x z) < fintype.card (Icc x y) :=
begin
have hxy : x ≤ y := le_of_lt (lt_of_le_of_lt hxz hzy),
have y_not_mem : y ∉ Icc x z := λ h, begin
simp only [hxy, true_and, mem_Icc] at h,
exact lt_irrefl _ (lt_of_le_of_lt h hzy),
end,
have y_mem : y ∈ Icc x y := by simp [hxy],
have : Icc x z ⊆ Icc x y := Icc_subset_Icc_right (le_of_lt hzy),
exact card_lt_card ⟨this, λ h, by cc⟩,
end

def μaux [decidable_eq α] (x : α) : α → R
| y := if x = y then 1 else begin
haveI : fintype (Ico x y) := sorry,
exact -finset.sum (fintype.elems (Ico x y)) (λ z,
have fintype.card ↥(Icc x z) < fintype.card ↥(Icc x y) :=
card_Icc_lt_card_Icc_of_lt α x y z.1 z.2.1 z.2.2,
μaux z),
end
using_well_founded {rel_tac := λ _ _, [exact ⟨_, measure_wf (λ y,
fintype.card (Icc x y)
)⟩]}

def μ [decidable_eq α] : incidence_algebra α R := λ x, μaux α R x

set_option pp.all false

example : μ ℕ ℤ = λ x y, if x = y then 1 else (if y = x + 1 then -1 else 0) :=
begin
ext x y,
split_ifs,
{dsimp [μ], rwa [μaux, if_pos], },
{dsimp [μ], rwa [μaux], rwa [if_neg, h_1], simp,
have : Ico x (x + 1) = {x} := sorry,
conv_lhs
{
rw [this],
congr,
skip,
funext,
rw [μaux],
rw [if_pos (sorry  : x = ↑ z)],
}, simp, have := (locally_finite.fin_Icc x (x+1)).complete, simp at this,
norm_cast,
rw finset.card_eq_one,
use x,
simp,
dsimp,
dunfold coe_sort,
dunfold has_coe_to_sort.coe,dsimp,
simp,
ext,
simp at a,
split,
intro h,

have := this x (by simp),
erw [(sorry : Icc x (x+1) = {x})] at this,  },
end
#eval μ ℕ ℤ 1 1
#check set.has_coe_to_sort
lemma (p) :  finset.sum (fintype.elems {x_1 : α // p x}) f

lemma μ_inv_ζ_eq_one [decidable_eq α] [@decidable_rel α (≤)] : μ α R * ζ α R = 1 := begin
ext x y,
dsimp,
simp [(*)],
unfold_coes,
dunfold coe_sort,
dunfold has_coe_to_sort.coe,dsimp,
simp,
end

#lint


#### Alex J. Best (Jun 20 2020 at 05:31):

Looks like list.Icc still isn't in mathlib, maybe we should add this as a (help wanted / easy) issue on github rather than just a comment in https://github.com/leanprover-community/mathlib/blob/fbc9592788fe71b15bdefc972a98f40b79d29bab/src/data/list/intervals.lean#L19 so people can find it?

#### Kevin Buzzard (Jun 20 2020 at 08:37):

Isn't pnat a canonically ordered comm monoid with a lattice structure? Won't this be enough for most things?

#### Kevin Buzzard (Jun 20 2020 at 08:40):

Note that nat isn't because of zero. But nat might well be a monoid with 0 with good factorisation properties. I was talking to @Chris Hughes about this the other day. The ideals in a commutative ring are a monoid and the ideals in a Dedekind domain are a monoid with a zero and, other than that, good factorisation properties. This all very much reminds me of @Johan Commelin 's group with 0 insight. There's some natural structure here that we're missing and we would like, but mathematicians didn't spot it yet. Is it an incidence algebra? I don't know what they are

#### Bryan Gin-ge Chen (Jun 20 2020 at 08:45):

Incidence algebras are what you define to generalize the Mobius inversion formula to settings like finite subsets where it becomes inclusion-exclusion.

#### David Wärn (Jun 20 2020 at 08:48):

Isn't nat a "canonically ordered comm monoid with lattice structure", where 0 is the maximal element? I think the problem with nat is that Dirichlet convolutions make no sense at 0, since a * b = 0 has infinitely many solutions

#### Kevin Buzzard (Jun 20 2020 at 09:08):

If the axioms work out for nat too then the situation is even better than I expected

#### Kevin Buzzard (Jun 20 2020 at 09:13):

The concept of a UFD generalises to monoids, was Chris' observation. And then there's this dichotomy depending on whether there's a 0 or not. At the end of the day the answer to the original question is that pnat as a monoid has the property that it is free, so you get all the juicy consequences of the universal property including a lattice structure with arbitrary nonzero infs. Does pnat have a lattice instance? Probably not because if there's an order it will be the usual one, not divisibility

#### David Wärn (Jun 20 2020 at 10:28):

I think there are at least three things happening with pnat that we can try to generalize:

• Dirichlet convolutions of arithmetic functions. Incidence algebras sort of make sense of this, but an element of the incidence algebra contains superfluous information. Another concept is this: given a ring R and a category C, such that every arrow in C has only finitely many factorisations into two arrows, we can form the "category algebra", which assigns a scalar in R to every arrow, and where convolution makes sense because of the finiteness condition. Given a monoid like pnat (but unlike nat under multiplication!) we can thus form the category algebra on the single object category, and get the usual notion of arithmetic function & Dirichlet convolution. We also get incidence algebras, since posets are categories. We get a "Zeta function" by assigning 1 to every arrow, and a "delta function" (identity for convolution) by assigning 1 to identity arrows and 0 to everything else.

• Multiplicative functions. Over "sufficiently nice" monoids (in particular free monoids like pnat), we can talk about multiplicative functions. I think for perfect numbers the relevant facts are "Zeta function is multiplicative", "the coercion pnat -> int is multiplicative", and "convolution of multiplicative functions is multiplicative".

• Möbius inversion.Sometimes we can find a Möbius function, inverse to the Zeta function. In particular it always exists in an incidence algebra.

#### Kevin Buzzard (Jun 20 2020 at 10:45):

It sounds like this incidence stuff is useful for the theory of so-called "multiplicative functions" (f(ab)=f(a)f(b) if gcd(a,b)=1), which do I think work on nat (f(0) can be anything). I wonder to what extent mobius inversion is useful though? I don't think you need it for perfect numbers

#### Kevin Buzzard (Jun 20 2020 at 10:49):

Note that the standard usage of the phrase in number theory books has this gcd condition -- a monoid hom is called a strictly multiplicative function in the number theory literature. Coefficients of certain modular forms are multiplicative but not monoid homs, somehow the weaker notion was isolated as being useful

#### David Wärn (Jun 20 2020 at 10:58):

Yes, multiplicative function is a good concept, but I'm not sure how it generalizes. Presumably there's a connection to be made with measures, which are only additive when your sets are disjoint

#### David Wärn (Jun 20 2020 at 11:01):

Meanwhile, the concept of category algebra generalizes matrix algebras (which I unsuccessfully tried to make sense of a while ago) as well, via indiscrete categories. What a concept!

#### David Wärn (Jun 20 2020 at 11:29):

I also don't think you need Möbius inversion for Perfect numbers -- but of course it's often useful for counting things. As far as I can see the main (only?) advantage of incidence algebras over category algebras is that you always have a Möbius function (the upshot of the category algebra is that you get the usual notion of arithmetic function).

#### Aaron Anderson (Jun 20 2020 at 16:25):

All you need right now for perfect numbers to work for pnats are some duplicate lemmas about gcd and stuff, which I’ve written, and an alteration of the fin_mult and coprime_part ideas to work with pnat.factors rather than multiplicity, which needs a semiring

#### Aaron Anderson (Jun 20 2020 at 16:26):

But I’m just thinking about how to avoid writing so many duplicate lemmas if I (or someone else) keeps writing related elementary number theory

#### Aaron Anderson (Jun 20 2020 at 18:09):

Kevin Buzzard said:

Isn't pnat a canonically ordered comm monoid with a lattice structure? Won't this be enough for most things?

This is likely what I'm looking for. There's no definition yet of a multiplicative canonically_ordered_comm_monoid, and maybe that's what I'm looking for... one problem I wouldn't know how to deal with is how to recognize dvd as a partial order, without interfering with the linear order le from the additive structure. Then also I'm not sure syntactically it'd be easy to prove things about the gcd function without just repeatedly rewriting gcd_eq_sup_dvd or something

#### Yury G. Kudryashov (Jun 20 2020 at 18:22):

AFAIR there is some theory about "dvd as a partial order" in algebra/associated.

#### Aaron Anderson (Jun 20 2020 at 19:54):

Yury G. Kudryashov said:

AFAIR there is some theory about "dvd as a partial order" in algebra/associated.

That does seem useful. I'd want to prove things about the special case where associates is a partial order, in bijection with the original monoid, because there's only one unit.

#### Aaron Anderson (Jun 21 2020 at 22:41):

I've retrofitted most of my file to deal with pnats, and created a new file, multiplicity_vectors.lean, that introduces yet another kind of prime factorisation (as a finsupp), but contains a lot of sorries

#### Aaron Anderson (Jun 21 2020 at 22:44):

This new factorisation would be pretty useful for talking about multiplicative functions, and maybe other things, I'm interested to see if anyone else is interested in it. Probably the next thing to do with that would be to show that it's order isomorphic and add_monoid isomorphic to factor_multiset, and then a bunch of the sorried properties will probably be reduced to lemmas saying that lattices respect order isomorphisms, which either should exist or do already

#### Johan Commelin (Jun 22 2020 at 05:03):

@Aaron Anderson Note that there is already an isomorphism between multiset X and finsupp X nat. You could use that to transport the definition and a bunch of lemmas...
Alternatively, we might decide that the finsupp approach is the more flexible point of view, and just ditch the multiset approach completely.

#### Aaron Anderson (Jun 22 2020 at 05:07):

I’ve used .to_multiset to define it, and I know that’s invertible and a strict_mono. Is that the isomorphism you’re referring to?

Yup, exactly

#### Johan Commelin (Jun 22 2020 at 05:08):

The inverse is .to_finsupp`

#### Aaron Anderson (Jul 01 2020 at 04:21):

I made a new commit, and started a PR review thread for 3094.

Last updated: May 14 2021 at 18:28 UTC