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.

@[reducible, inline]

abbrev 𝔽 (p n : ℕ) : Type

𝔽 p n is the vector space (Z/pZ)^n. When p is prime, this is $\mathbb{F}_p^n$.

Equations

• 𝔽 p n = (Fin n → ZMod p)

@[reducible, inline]

abbrev 𝔽₂ (n : ℕ) : Type

𝔽₂ n is the vector space $\mathbb{F}_2^n$.

Equations

• 𝔽₂ n = 𝔽 2 n

@[reducible, inline]

abbrev 𝔽₃ (n : ℕ) : Type

𝔽₃ n is the vector space $\mathbb{F}_3^n$.

Equations

• 𝔽₃ n = 𝔽 3 n

@[reducible, inline]

abbrev 𝔽₅ (n : ℕ) : Type

𝔽₅ n is the vector space $\mathbb{F}_5^n$.

Equations

• 𝔽₅ n = 𝔽 5 n

@[reducible, inline]

abbrev 𝔽₇ (n : ℕ) : Type

𝔽₇ n is the vector space $\mathbb{F}_7^n$.

Equations

• 𝔽₇ n = 𝔽 7 n