Probe: universe-free binder
ProvedWeil.zzz_probe_mononumber-theory
A finite field has a nonzero number of elements. 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
Formal statement
namespace Weil
theorem zzz_probe_mono : ∀ {F : Type} [Field F] [Fintype F], Fintype.card F ≠ 0 := by sorry
end Weil