Probe: universe-free binder

Proved

Weil.zzz_probe_mono

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

number-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