1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42

import Mathlib

example (n : ℕ) (k : ℕ) (h : k ≤ n) : ∃ C : List ℕ, C.length = k ∧ C.Chain' (· < ·) ∧ (C.mapIdx (fun c i => c.choose i) |>.sum) = n := by
  induction k
--   · use []

def fieldSum F [Field F] [Fintype F] := ∑ i : F, i

def F32 := GaloisField 2 5

-- noncomputable instance : Field F32 :=
--   inferInstanceAs (Field (Polynomial.SplittingField _))



-- noncomputable instance : Finite F32 :=
--   Module.finite_of_finite (ZMod 2)

noncomputable instance : Fintype (GaloisField 2 5) :=
  Fintype.ofFinite (GaloisField 2 5)

#eval fieldSum <| GaloisField 2 5


def groupSum G [AddCommGroup G] [Fintype G] := ∑ i : G, i

#eval Functor

def L := List.range' 1 100


#eval (fun n [NeZero n] => ∑ i : ZMod n, i) 10

example n [NeZero n] : ∑ i : ZMod n, i = if n % 2 = 0 then n / 2 else 0 := by
  if h : n % 2 = 0 then
    simp [h]
    grind
  else
    simp [h]
    grind

#eval L.map fun j [NeZero j] => ∑ i : ZMod j, i