feat(FormalConjecturesForMathlib): Introduce 𝔽 notation

FormalConjectures/GreensOpenProblems/19.lean

@@ -51,8 +51,6 @@ noncomputable def S (d : G) (A : Finset (G × G)) : Finset (G × G) :=
 
 end GroupDefs
 
-/-- The group $G = \mathbb{F}_2^n = (Z/2Z)^n$. -/
-abbrev 𝔽₂ (n : ℕ) := Fin n → ZMod 2
 
 /--
 True if the given exponent satisfies Green's conditions [Gr26].

FormalConjectures/GreensOpenProblems/26.lean

@@ -33,11 +33,6 @@ open scoped Pointwise
 
 namespace Green26
 
-/-- The vector space $\mathbb{F}_p^n$. -/
-abbrev 𝔽 (p n : ℕ) [Fact p.Prime] := Fin n → ZMod p
-
-/-- The vector space $\mathbb{F}_3^n$. -/
-abbrev 𝔽₃ (n : ℕ) := 𝔽 3 n
 
 /-- The standard cube in $\mathbb{F}_p^n$ is the set of points with coordinates in $\{0, 1\}$. -/
 def StandardCube {p : ℕ} [Fact p.Prime] (n : ℕ) : Set (𝔽 p n) :=

FormalConjectures/GreensOpenProblems/31.lean

@@ -137,8 +137,8 @@ where $N = 2^n$ [Gr24].
 -/
 @[category research open, AMS 5 11]
 theorem green_31.variants.sidon_01n : answer(sorry) ↔
-    ∃ S : (n : ℕ) → Finset (Fin n → ZMod 2),
-      (∀ n, IsSidon (S n : Set (Fin n → ZMod 2))) ∧
+    ∃ S : (n : ℕ) → Finset (𝔽₂ n),
+      (∀ n, IsSidon (S n : Set (𝔽₂ n))) ∧
       ∀ᶠ n in atTop, ((2 : ℝ) ^ n) ^ (0.51 : ℝ) ≤ (S n).card := by
   sorry
 
@@ -147,8 +147,8 @@ The best-known upper bound for a Sidon subset of $\{0, 1\}^n$ ($N = 2^n$) is $N^
 -/
 @[category research solved, AMS 5 11]
 theorem green_31.variants.sidon_01n_clz01 :
-    ∃ C : ℝ, ∀ n, ∀ S : Finset (Fin n → ZMod 2),
-      IsSidon (S : Set (Fin n → ZMod 2)) → (S.card : ℝ) ≤ C * ((2 : ℝ) ^ n) ^ (0.5753 : ℝ) := by
+    ∃ C : ℝ, ∀ n, ∀ S : Finset (𝔽₂ n),
+      IsSidon (S : Set (𝔽₂ n)) → (S.card : ℝ) ≤ C * ((2 : ℝ) ^ n) ^ (0.5753 : ℝ) := by
   sorry
 
 end Green31

FormalConjectures/GreensOpenProblems/32.lean

@@ -135,14 +135,14 @@ theorem green_32.variants.log_regime :
 A set $A$ has a coset hole of size $L$ if there exists a subspace $W$ and a vector $v$ such that
 the affine space $v + W$ has size at least $L$ and is disjoint from $A$.
 -/
-def HasCosetHole {n : ℕ} (A : Finset (Fin n → ZMod 2)) (L : ℕ) : Prop :=
-  ∃ W : Submodule (ZMod 2) (Fin n → ZMod 2), ∃ v : Fin n → ZMod 2,
-    L ≤ Nat.card W ∧ ∀ w : W, v + (w : Fin n → ZMod 2) ∉ A
+def HasCosetHole {n : ℕ} (A : Finset (𝔽₂ n)) (L : ℕ) : Prop :=
+  ∃ W : Submodule (ZMod 2) (𝔽₂ n), ∃ v : 𝔽₂ n,
+    L ≤ Nat.card W ∧ ∀ w : W, v + (w : 𝔽₂ n) ∉ A
 
 /-- The empty set in $\mathbb{F}_2^n$ has a coset hole (using the trivial subspace). -/
 @[category test, AMS 5 11]
 theorem hasCosetHole_empty (n : ℕ) :
-    HasCosetHole (∅ : Finset (Fin n → ZMod 2)) 0 := by
+    HasCosetHole (∅ : Finset (𝔽₂ n)) 0 := by
   exact ⟨⊥, 0, Nat.zero_le _, fun _ => by simp⟩
 
 /--
@@ -153,7 +153,7 @@ size at least $100\sqrt{N}$ for sufficiently large $n$.
 @[category research solved, AMS 5 11]
 theorem green_32.variants.finite_field :
     ∀ᶠ n in atTop,
-      ∀ A : Finset (Fin n → ZMod 2), A.card = ⌊Real.sqrt (2^n : ℝ)⌋₊ →
+      ∀ A : Finset (𝔽₂ n), A.card = ⌊Real.sqrt (2^n : ℝ)⌋₊ →
       HasCosetHole A ⌊100 * Real.sqrt (2^n : ℝ)⌋₊ := by
   sorry
 

FormalConjectures/GreensOpenProblems/38.lean

@@ -32,8 +32,6 @@ open scoped Pointwise
 
 namespace Green38
 
-/-- The vector space $\mathbb{F}_7^n$. -/
-abbrev 𝔽₇ (n : ℕ) := Fin n → ZMod 7
 
 /-- $A - A$ intersects $\{-1, 0, 1\}^n$ only at $0$. -/
 def IntersectsOnlyAtZero {n : ℕ} (A : Finset (𝔽₇ n)) : Prop :=

FormalConjectures/GreensOpenProblems/40.lean

@@ -34,8 +34,6 @@ open scoped ENNReal Pointwise
 
 namespace Green40
 
-/-- The vector space $\mathbb{F}_2^n$. -/
-abbrev 𝔽₂ (n : ℕ) := Fin n → ZMod 2
 
 /-- The Hamming ball of radius $r$ in $\mathbb{F}_2^n$. -/
 def hammingBall (n r : ℕ) : Set (𝔽₂ n) :=

FormalConjectures/GreensOpenProblems/49.lean

@@ -39,8 +39,6 @@ open scoped Pointwise Finset
 
 namespace Green49
 
-/-- The vector space $\mathbb{F}_2^n$. -/
-abbrev 𝔽₂ (n : ℕ) := Fin n → ZMod 2
 
 /--
 Suppose that $A \subset \mathbb{F}_2^n$ is a set with $|A + A| \leq K|A|$. Is it true that $A$

FormalConjectures/GreensOpenProblems/50.lean

@@ -49,11 +49,11 @@ over $\mathbb{F}_2$.
 -/
 @[category research open, AMS 5 11]
 theorem green_50 : answer(sorry) ↔
-    ∃ C > (0 : ℝ), ∀ n : ℕ, ∀ A : Finset (Fin n → ZMod 2),
+    ∃ C > (0 : ℝ), ∀ n : ℕ, ∀ A : Finset (𝔽₂ n),
     A.Nonempty →
     let α : ℝ := A.dens
-    ∃ (W : Submodule (ZMod 2) (Fin n → ZMod 2)) (v : Fin n → ZMod 2),
-      v +ᵥ (W : Set (Fin n → ZMod 2)) ⊆ ↑(10 • A) ∧
+    ∃ (W : Submodule (ZMod 2) (𝔽₂ n)) (v : 𝔽₂ n),
+      v +ᵥ (W : Set (𝔽₂ n)) ⊆ ↑(10 • A) ∧
       (n : ℝ) - C * Real.logb 2 (1 / α) ≤ Module.finrank (ZMod 2) W := by
   sorry
 

FormalConjectures/GreensOpenProblems/51.lean

@@ -36,8 +36,6 @@ open scoped Pointwise
 
 namespace Green51
 
-/-- The group $G = \mathbb{F}_2^n = (Z/2Z)^n$. -/
-abbrev 𝔽₂ (n : ℕ) := Fin n → ZMod 2
 
 /-- The maximum dimension of a coset contained in the set $A$. -/
 noncomputable def maxCosetDim (n : ℕ) (A : Set (𝔽₂ n)) : ℕ :=

FormalConjectures/GreensOpenProblems/9.lean

@@ -59,7 +59,7 @@ Problem 9 (iii): is $r_4(\mathbf{F}_5^n) \ll N^{1-c}$, where $N=5^n$?
 -/
 @[category research open, AMS 5]
 theorem green_9_iii : answer(sorry) ↔
-    ∃ c > (0 : ℝ), (fun (n : ℕ) ↦ ((Finset.univ : Finset (Fin n → ZMod 5)).maxAPFreeCard 4 : ℝ))
+    ∃ c > (0 : ℝ), (fun (n : ℕ) ↦ ((Finset.univ : Finset (𝔽₅ n)).maxAPFreeCard 4 : ℝ))
       ≪ fun (n : ℕ) ↦ ((5 : ℝ) ^ n) ^ (1 - c) := by
   sorry
 

FormalConjecturesForMathlib.lean

@@ -103,6 +103,7 @@ public import FormalConjecturesForMathlib.Data.Real.NearestInt
 public import FormalConjecturesForMathlib.Data.Set.Density
 public import FormalConjecturesForMathlib.Data.Set.Interval
 public import FormalConjecturesForMathlib.Data.Set.Triplewise
+public import FormalConjecturesForMathlib.Data.ZMod.Fp
 public import FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet
 public import FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs
 public import FormalConjecturesForMathlib.Geometry.Euclidean

FormalConjecturesForMathlib/Data/ZMod/Fp.lean

@@ -0,0 +1,43 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.Data.ZMod.Basic
+
+@[expose] public section
+
+/-!
+# Notation for finite field vector spaces
+
+This file defines the notation `𝔽 p n` for the vector space `Fin n → ZMod p`
+over the finite field of order `p`, and provides standard abbreviations for
+small primes.
+-/
+
+/-- `𝔽 p n` is the vector space `(Z/pZ)^n`. When `p` is prime, this is $\mathbb{F}_p^n$. -/
+abbrev 𝔽 (p n : ℕ) := Fin n → ZMod p
+
+/-- `𝔽₂ n` is the vector space $\mathbb{F}_2^n$. -/
+abbrev 𝔽₂ (n : ℕ) := 𝔽 2 n
+
+/-- `𝔽₃ n` is the vector space $\mathbb{F}_3^n$. -/
+abbrev 𝔽₃ (n : ℕ) := 𝔽 3 n
+
+/-- `𝔽₅ n` is the vector space $\mathbb{F}_5^n$. -/
+abbrev 𝔽₅ (n : ℕ) := 𝔽 5 n
+
+/-- `𝔽₇ n` is the vector space $\mathbb{F}_7^n$. -/
+abbrev 𝔽₇ (n : ℕ) := 𝔽 7 n