Finset card question

Stream: mathlib4

[Sorrachai Yingchareonthawornchai]

I define an n-by-n matrix as M (i j : Fin n) : Prop := i.val = 0 ∨ j.val = 0.
I want to count the number of 1's (True) in M which is 2n-1. Is there an easy way to count?

For my purpose, I would need only to prove only the lower bound of it.
Let t := (filter (fun (i,j) ↦ M i j) univ)
have : 2*n - 1 ≤ t.card

Following Yaël's advice, I plan to use an injective map

let s : Finset ℤ := Icc (-n + 1) (n - 1)
let f : Finset ℤ → Fin n × Fin n  := fun (i) ↦ ( posPart i , negPart i) --- this line said it failed to synthesize
  AddGroup (Fin n)

Any advice on how to proceed would be appreciated. Thanks.

[Kevin Buzzard]

What's the full error?

[Sorrachai Yingchareonthawornchai]

application type mismatch
i⁺
argument
i
has type
Finset ℤ : Type
but is expected to have type
Fin n : Type

[Kevin Buzzard]

I think that's a pretty clear description of why your code doesn't work

[Yaël Dillies]

The codomain should be \Z, not Finset \Z

[Kevin Buzzard]

Domain not codomain?

[Sorrachai Yingchareonthawornchai]

Thanks.
application type mismatch
i⁺
argument
i
has type
ℤ : Type
but is expected to have type
Fin n : Type

[Sorrachai Yingchareonthawornchai]

So it does not automatically cast an integer to Fin n?

[Kevin Buzzard]

There's no coercion if n=0 which isn't ruled out

[Sorrachai Yingchareonthawornchai]

I see thanks a lot

[Kevin Buzzard]

Once you figure out how to get around this (ie by making the assumption which the coercion is expecting to see, in a way which it can see it) then the code will work

[Kevin Buzzard]

Unfortunately I'm not at a computer so can only guess. [NeZero n]?

[Sorrachai Yingchareonthawornchai]

It works now thanks! Somehow the error message does not say much.

[Sorrachai Yingchareonthawornchai]

Another question:

• let f : ℤ → Fin n × Fin n := fun (i) ↦ ( posPart i , negPart i)
• in my tactic state, it shows f : ℤ → Fin n × Fin n := fun i ↦ ((↑i)⁺, (↑i)⁻)
• but it should be f : ℤ → Fin n × Fin n := fun i ↦ (↑(i⁺), ↑(i⁻))? And how do I enforce this?

[Yaël Dillies]

Write let f (i : ℤ) : Fin n × Fin n := (↑(i⁺), ↑(i⁻))