convert in base_7

Stream: new members

[liu]

Now I have a number, say 629. I want to convert it to a number in base - 7 and store each digit of this number in a set. How should I do it?

[Johan Commelin]

I think docs#Nat.digits is what you want.

[liu]

I still don't understand how to convert a decimal number to a septenary (base - 7) number and get each digit of it. Can you give me an example?

[Johan Commelin]

import Mathlib.Data.Nat.Digits

#eval Nat.digits 7 629
-- [6, 5, 5, 1]

[liu]

What should I do to convert this list into a set?

import Mathlib
example(set1:Finset ℕ )(set2:Finset ℕ )(set3:Finset ℕ )(n:ℕ )(h0:n=629)(h1:set1=Nat.digits 7 629)(h2:Nat.digits 8 629):{n:ℕ | n ∈ (set1 ∩ set2) }.ncard=3:=by sorry

[Moritz Firsching]

there is toFinset, so you can do something like this:

import Mathlib
example (set1:Finset ℕ )(set2:Finset ℕ )(set3:Finset ℕ )(n:ℕ )(h0:n=629)
   (h1:set1 = (Nat.digits 7 629).toFinset)(h2: set2 = (Nat.digits 8 629).toFinset):
   {n:ℕ | n ∈ (set1 ∩ set2) }.ncard=3:=by
   rw [h1, h2]
   have : {n | n = 5 ∨ n = 6 ∨ n = 1} = {5, 6, 1} := by rfl
   simp [this]

[Moritz Firsching]

but instead of {n:ℕ | n ∈ (set1 ∩ set2) }.ncard, perhaps you rather want directly (set1 ∩ set2).card?

[Moritz Firsching]

with better spacing, removing superflous assumption, and actually using n=629 it would look like this:

import Mathlib
example (set1 : Finset ℕ) (set2 : Finset ℕ) (n : ℕ) (h0 : n = 629)
   (h1 : set1 = (Nat.digits 7 n).toFinset)(h2 : set2 = (Nat.digits 8 n).toFinset):
   (set1 ∩ set2).card = 3 := by
   simp [h0, h1, h2]