Documentation

PFR.ForMathlib.Elementary

Finite field vector spaces #

Here we define the notion of a vector space over a finite field, and record basic results about it.

Main classes #

source
class ElementaryAddCommGroup (G : Type u_1) [AddCommGroup G] (p : outParam ℕ) :
Prop

An elementary p-group, i.e., a commutative additive group in which every nonzero element has order exactly p.

Instances
    source
    theorem ElementaryAddCommGroup.orderOf_of_ne {G : Type u_1} [AddCommGroup G] {p : outParam ℕ} [self : ElementaryAddCommGroup G p] {x : G} (hx : x ≠ 0) :
    addOrderOf x = p
    source
    @[simp]
    theorem ElementaryAddCommGroup.torsion {G : Type u_1} [AddCommGroup G] (p : ℕ) [elem : ElementaryAddCommGroup G p] (x : G) :
    p • x = 0
    source
    theorem ElementaryAddCommGroup.of_torsion {G : Type u_1} [AddCommGroup G] {p : ℕ} (hp : p.Prime) (h : ∀ (x : G), p • x = 0) :
    ElementaryAddCommGroup G p
    source
    theorem ElementaryAddCommGroup.ofModule {G : Type u_1} {p : ℕ} [AddCommGroup G] [Module (ZMod p) G] [Fact p.Prime] :
    ElementaryAddCommGroup G p

    A vector space over Z/p is an elementary abelian p-group.

    source
    @[instance 100]
    instance ElementaryAddCommGroup.module {G : Type u_1} {n : ℕ} [AddCommGroup G] [ElementaryAddCommGroup G n] :
    Module (ZMod n) G
    Equations
    source
    instance ElementaryAddCommGroup.instOfNatNatOfModuleZMod {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] :
    ElementaryAddCommGroup G 2
    Equations
    • ⋯ = ⋯
    source
    theorem ElementaryAddCommGroup.exists_subgroup_subset_card_le {G : Type u_1} {p : ℕ} (hp : p.Prime) [AddCommGroup G] [h : ElementaryAddCommGroup G p] {k : ℕ} (H : AddSubgroup G) (hk : k ≤ Nat.card ↥H) (h'k : k ≠ 0) :
    ∃ (H' : AddSubgroup G), Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

    In an elementary abelian $p$-group, every finite subgroup $H$ contains a further subgroup of cardinality between $k$ and $pk$, if $k \leq |H|$.

    source
    @[simp]
    theorem ElementaryAddCommGroup.sub_eq_add {G : Type u_1} [AddCommGroup G] [elem : ElementaryAddCommGroup G 2] (x : G) (y : G) :
    x - y = x + y
    source
    @[simp]
    theorem ElementaryAddCommGroup.add_self {G : Type u_1} [AddCommGroup G] [elem : ElementaryAddCommGroup G 2] (x : G) :
    x + x = 0
    source
    @[simp]
    theorem ElementaryAddCommGroup.neg_eq_self {G : Type u_1} [AddCommGroup G] [elem : ElementaryAddCommGroup G 2] (x : G) :
    -x = x
    source
    theorem ElementaryAddCommGroup.sum_add_sum_eq_sum {G : Type u_1} [AddCommGroup G] [elem : ElementaryAddCommGroup G 2] (x : G) (y : G) (z : G) :
    x + y + (y + z) = x + z
    source
    theorem ElementaryAddCommGroup.sum_add_sum_add_sum_eq_zero {G : Type u_1} [AddCommGroup G] [elem : ElementaryAddCommGroup G 2] (x : G) (y : G) (z : G) :
    x + y + (y + z) + (z + x) = 0
    source
    @[simp]
    theorem ElementaryAddCommGroup.char_smul_eq_zero {p : ℕ} {Γ : Type u_1} [AddCommGroup Γ] [ElementaryAddCommGroup Γ p] (x : Γ) :
    p • x = 0
    source
    theorem ElementaryAddCommGroup.char_ne_one_of_ne_zero {p : ℕ} {Γ : Type u_1} [AddCommGroup Γ] [ElementaryAddCommGroup Γ p] {x : Γ} (x_ne_zero : x ≠ 0) :
    p ≠ 1
    source
    @[simp]
    theorem ElementaryAddCommGroup.char_smul_eq_zero' {p : ℕ} {Γ : Type u_1} [AddCommGroup Γ] [ElementaryAddCommGroup Γ p] (x : Γ) (k : ℤ) :
    (k * ↑p) • x = 0
    source
    theorem ElementaryAddCommGroup.two_le_char_of_ne_zero {p : ℕ} {Γ : Type u_1} [NeZero p] [AddCommGroup Γ] [ElementaryAddCommGroup Γ p] {x : Γ} (x_ne_zero : x ≠ 0) :
    2 ≤ p
    source
    theorem ElementaryAddCommGroup.mem_periodicPts {p : ℕ} {Γ : Type u_1} [NeZero p] [AddCommGroup Γ] [ElementaryAddCommGroup Γ p] {x : Γ} (y : Γ) :
    y ∈ Function.periodicPts fun (z : Γ) => x + z
    source
    instance ElementaryAddCommGroup.instForallOfNeZeroNat (Ω : Type u_1) (Γ : Type u_2) (p : ℕ) [NeZero p] [AddCommGroup Γ] [ElementaryAddCommGroup Γ p] :
    ElementaryAddCommGroup (Ω → Γ) p
    Equations
    • ⋯ = ⋯
    source
    theorem ElementaryAddCommGroup.Int.mod_eq (n : ℤ) (m : ℤ) :
    n % m = n - n / m * m
    source
    theorem ElementaryAddCommGroup.exists_finsupp {G : Type u_1} [AddCommGroup G] {n : ℕ} [ElementaryAddCommGroup G (n + 1)] {A : Set G} {x : G} (hx : x ∈ Submodule.span ℤ A) :
    ∃ (μ : ↑A →₀ ZMod (n + 1)), (μ.sum fun (a : ↑A) (r : ZMod (n + 1)) => r.cast • ↑a) = x
    source
    theorem ElementaryAddCommGroup.finite_closure {G : Type u_1} [AddCommGroup G] {n : ℕ} [ElementaryAddCommGroup G (n + 1)] {A : Set G} (h : A.Finite) :
    (↑(AddSubgroup.closure A)).Finite
    source
    theorem ElementaryAddCommGroup.subgroup {G : Type u_1} [AddCommGroup G] {n : ℕ} [ElementaryAddCommGroup G n] (H : AddSubgroup G) :
    ElementaryAddCommGroup (↥H) n
    source
    theorem ElementaryAddCommGroup.quotient_group {G : Type u_1} [AddCommGroup G] {p : ℕ} (hp : p.Prime) {H : AddSubgroup G} (hH : ∀ (x : G), p • x ∈ H) :
    ElementaryAddCommGroup (G ⧸ H) p