Random broken binomial stuff

Changes

1 changed files (+42/-0)

• Binom.lean (new)
  • @@ -0,0 +1,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