factors lemma

Stream: Is there code for X?

[Ines Wright]

Is there a lemma that says the list of factors of a prime to a power is the prime, n times?

import data.nat.prime

example {p y : ℕ} [p.prime] : (p ^ y).factors = list.repeat p y :=
begin
  sorry,
end

[Eric Rodriguez]

this should be in another thread - Zulip can be confusing! but no, should be pretty straightforward though

[Eric Rodriguez]

this is docs#nat.factors, right?

[Johan Commelin]

@Ines Wright Hi! Would you mind editing your message to change it's topic to a new thread name?

[Johan Commelin]

There is docs#nat.factors_prime, but I couldn't find nat.factors_mul.

[Kevin Buzzard]

The problem with nat.factors_mul is that nat.factors is a list not a multiset, presumably for CS reasons.

[Kevin Buzzard]

So you'd have to state it with ~ rather than =. I could imagine trying to use FTA to prove it by saying "list.repeat p y has the property that its prod is p^y so done by FTA" but then you have to prove that if list.repeat p y ~ L then list.repeat p y = L. Is this in mathlib?

[Kevin Buzzard]

docs#nat.factors_unique

[Eric Wieser]

docs#list.repeat_perm

[Yakov Pechersky]

Kevin, nat.factors is a list gives you the additional nice property that it is in increasing order.

[Kevin Buzzard]

yeah but given a multiset I'm sure any CS person can put it into increasing order if they _want_...

[Kevin Buzzard]

and you can see that it screws up nat.factors_mul ;-)

[Kevin Buzzard]

More seriously, to a mathematician the "canonical" way of expressing the factors of a natural is as a multiset, because this is precisely the kind of data which can be canonically associated to the natural. When thinking of the factors there's no conceptual reason to include the ordering.

[Eric Wieser]

There's also docs#pnat.factor_multiset

[Eric Wieser]

Which also fixes the weirdness where factors 1 = factors 0 despite it not being the case that 1 = 0

[Eric Rodriguez]

pnat factor multiset is a PITA

[Eric Rodriguez]

from having looked at this bit of mathlib lately the best rn is definitely docs#nat.factors_subset_right, but that's miles off

[Yaël Dillies]

All this pnat part of mathlib has been written a few years and is never used anywhere. Parts of it are poorly written and others are redundant with more general stuff. That's my take. But yeah I guess you can use it and give it some love.

[Yaël Dillies]

See #7960 for a more thorough explanation of mine.

[Yakov Pechersky]

We can redefine factors as the multiset via quotient.mk, and retain the original as factors_list

[Yakov Pechersky]

We don't have a multiset.repeat?

[Eric Rodriguez]

i think the smul is repeat, basically

[Eric Rodriguez]

no clue where it's defined, though

[Eric Rodriguez]

yep:

import data.multiset
def asdg : multiset ℕ := 4 • (quotient.mk $ [1,2,3,4])
#reduce asdg
-- quot.mk list.perm [1, 2, 3, 4, 1, 2, 3, 4, 1, 2, 3, 4, 1, 2, 3, 4]

[Eric Rodriguez]

it's just the default smul, which makes a lot of sense as add is just appending two multisets

[Ruben Van de Velde]

There's also docs#multiset.repeat

[Eric Rodriguez]

sadly they're not defeq, but probably a lemma that should be in mathlib:

lemma asda {α : Type*} (a : α) : ∀ n, multiset.repeat a n = n • {a}
| 0 := rfl
| (n + 1) := by simp [asda n, succ_nsmul]

[Kevin Buzzard]

lemma foo (p y : ℕ) [hp : p.prime] :   (p ^ y).factors = list.repeat p y := sorry

I have a proof -- but did we yet decide on whether this lemmas is called factors_pow_prime or prime_pow_factors or what?

[Adam Topaz]

prime_pow_factors sounds good to me!

[Mario Carneiro]

I would go with prime.factors_pow where hp is explicit