compute the number of elements in a finite set

Stream: new members

[MemoryExist]

F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
q : ℕ
k : Odd q
h : q = Fintype.card F
sq' : Set F := {x | x ^ ((q - 1) / 2) - 1 = 0 ∨ x = 0}
⊢ sq'.ncard = (q + 1) / 2

[Riccardo Brasca]

Can you please use #backticks?

[Riccardo Brasca]

And give a #mwe, not just the goal.

[Ruben Van de Velde]

And, maybe, ask a question or explain what you've done so far rather than just dumping some output

[MemoryExist]

import Mathlib


example { F : Type*}[Field F][Fintype F](q : ℕ)(k : Odd  q)(h: q = Fintype.card F)(set sq':={x:F | x ^ ((q - 1) / 2) - 1 = 0 ∨ x=0}):sq'.ncard=(q+1)/2:=by sorry

[Johannes Tantow]

import Mathlib

theorem test { F : Type*}[Field F][Fintype F](q : ℕ)(k : Odd  q)(h: q = Fintype.card F)(set sq':={x:F | x ^ ((q - 1) / 2) - 1 = 0 ∨ x=0}):sq'.ncard=(q+1)/2:=by sorry

example : False := by
  have := test (F:= ZMod 3) 3 (by simp[Odd]) (by simp) ∅ ∅
  simp at this

[Johannes Tantow]

set and sq are optional parameters, so I can set them with any set I want and then your theorem does not hold.

[MemoryExist]

Johannes Tantow 发言道：

set and sq are optional parameters, so I can set them with any set I want and then your theorem does not hold.

sorry that I made a mistake, but,actually I want to proof that the card of set sq:={x:F | x ^ ((q - 1) / 2) - 1 = 0 ∨ x=0} is (q+1)/2

[Yicheng Tao]

I think the proper statement should be:

import Mathlib

example { F : Type*} [Field F] [Fintype F] (q : ℕ) (k : Odd  q) (h: q = Fintype.card F) :
  {x : F | x ^ ((q - 1) / 2) - 1 = 0 ∨ x = 0 }.ncard = (q + 1) / 2 := by sorry