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):
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