Zulip Chat Archive

Stream: new members

Topic: Get Finsupp with all factors less than given number?


Ilmārs Cīrulis (Dec 20 2024 at 20:38):

Hello!

There's this beautiful thing Nat.factorization. How can I make the function that filters out all divisors bigger than given number and make new ℕ →₀ ℕ?

Smth like this unfinished effort:

def divisors_under_i (i: ):    →₀  := by
  intros n
  refine Finsupp.mk ?_ (λ x => if x  i then n.factorization x else 0) ?_
  . sorry
  . sorry

Ilmārs Cīrulis (Dec 20 2024 at 20:38):

Thanks in advance!

Edward van de Meent (Dec 20 2024 at 20:41):

firstly, since you're defining data, using tactics is a bad idea. secondly, Finsupp.filter should allow you to get basically what you want.

Ruben Van de Velde (Dec 20 2024 at 20:41):

docs#Finsupp.filter

Ruben Van de Velde (Dec 20 2024 at 20:42):

Edward beat me to it, but I guessed the same name and it seems appropriate

Ilmārs Cīrulis (Dec 20 2024 at 20:47):

Why are tactics bad idea (in this case)?

I'm sure that what the tactics have made in this case, is fun n => Finsupp.mk _ (fun x => blabla) _.

Ilmārs Cīrulis (Dec 20 2024 at 20:47):

#print divisors_under_i confirmed this

Ilmārs Cīrulis (Dec 20 2024 at 20:49):

If that's really necessary, I can avoid tactics, sure.

Ruben Van de Velde (Dec 20 2024 at 21:00):

Yeah, intro, refine, exact are all fine

Ruben Van de Velde (Dec 20 2024 at 21:01):

It's just a bit of an orange flag, because using more complex tactics in the definition makes it harder to prove things about it

Ilmārs Cīrulis (Dec 20 2024 at 21:07):

Ok, it seems I have finished it. Thank you!

import Mathlib

def divisors_under_i (i n: ):  →₀  :=
  Finsupp.mk
   (n.factorization.support.filter (λ x => x  i))
   (fun x => if x  i then n.factorization x else 0)
   (by simp; intros a; constructor <;> simp
       . intros H1 H2 H3 H4
         refine H4, λ H5 => ?_⟩
         rw [Nat.Prime.dvd_iff_one_le_factorization H1 H3, H5] at H2
         exact Nat.not_succ_le_zero 0 H2
       . intros H1 H2
         rw [Nat.factorization_eq_zero_iff] at H2
         simp at H2
         refine H2, H1
   )

Edward van de Meent (Dec 20 2024 at 21:10):

how about

def divisors_under_i (i n: ):  →₀  := n.factorization.filter (fun p => p  i)

Ruben Van de Velde (Dec 20 2024 at 21:11):

:snail:

Edward van de Meent (Dec 20 2024 at 21:12):

i suspect this will give better api

Ilmārs Cīrulis (Dec 20 2024 at 21:15):

Yes, this looks like 100 times more reasonable


Last updated: May 02 2025 at 03:31 UTC