Probe: universe-polymorphic binder
ProvedWeil.zzz_probe_polynumber-theory
A finite field has a nonzero number of elements, stated for a field in an arbitrary universe. Submitted as an infrastructure probe while diagnosing a verifier issue; will be retired.
Preamble
import Mathlib.Algebra.Field.Basic import Mathlib.Data.Fintype.Card set_option autoImplicit false universe u_1
Formal statement
namespace Weil
theorem zzz_probe_poly : ∀ {F : Type u_1} [Field F] [Fintype F], Fintype.card F ≠ 0 := by sorry
end Weil