convert cardinals to integer

Stream: new members

[Rahul Saha]

Hey guys, I am trying to formalize some quadratic forms definitions in Lean 3.0 (mostly for my own amusement) and ran into this hurdle. For a positive-definite quadratic form f, I am trying to define the representation number of an integer m in the following way.

def representation_set (f: binary_quadratic_form) (m: ℤ) : set (ℤ × ℤ)  :=
{xy : ℤ × ℤ | Q f xy.1 xy.2 = m}

def representation_number (f: binary_quadratic_form) (hyp: is_positive_definite f) (m: ℤ) : cardinal
:= cardinal.mk (representation_set f m)

Here, I first define representation_set as the set of all solutions of f(xy) = m, and then define the representation number as the cardinality of this set. However, the output of cardinal.mk is a cardinal object, but I want it to be an integer (subject to the hypothesis that f is positive definite). Is there a way to convert the cardinal to an integer? Or is there another way that I should be approaching this definition? Thanks in advance!

[Alex J. Best]

It sounds like making your definition via docs#set.ncard instead is what you want

[Alex J. Best]

Then the definition will not require any hypotheses but your theorems about that definition might (or might not!)

[Rahul Saha]

Ah gotcha, thanks!

[Ruben Van de Velde]

And I'm assuming that you don't actually mean 3.0

[Rahul Saha]

oh huh when I printed lean --version it gave me Lean (version 3.50.3, commit 855e5b74e3a5, Release)

[Rahul Saha]

Hm, it raises invalid import when I try to import data.set.ncard @Alex J. Best

[Rahul Saha]

ah, it seems that my _target folder does not contain the latest mathlib files

[Rahul Saha]

okay I got the imports sorted out,

def representation_number_int (f: binary_quadratic_form) (hyp: is_positive_definite f) (m: ℤ) : ℕ
:=  ncard (representation_set f m)

But now it says missing 'noncomputable' modifier, definition depends on set.ncard.

[Rahul Saha]

okay the following seems like it worked

noncomputable def representation_number_int (f: binary_quadratic_form) (hyp: is_positive_definite f) (m: ℤ) : ℕ
:=  ncard (representation_set f m)

But what exactly does noncomputable do in Lean?

[Kevin Buzzard]

It puts Lean into maths mode.

[Kevin Buzzard]

It means "you don't have to supply the algorithm which computes this number"

[Eric Rodriguez]

Lean tries to compute where it can, but set.ncard is not really something computable (what is the size of the set {0, 0 if RH else 1}? so you have to tell Lean "don't even try"

[Rahul Saha]

ah, haha gotcha that makes sense, thanks guys