Theorem: Matroid.kung (Matroid/Old/Kung.lean)

State before:
α : Type u_1
M✝ : Matroid α
q : ℕ
M : Matroid α
hM : ¬sorryAx Prop true
⊢ M.numPoints ≤ ↑(∑' (i : { i // ↑i ≤ M.erk }), q ^ ↑i)
Tactic:
_
State after:
no goals