Brauer groups over finite fields

This file proves that the Brauer group of a finite field is trivial.

theorem BrauerTrivial (K : Type u_1) [Field K] [Finite K] (A : CSA K) : ∃ (n : ℕ), n ≠ 0 ∧ Nonempty (↑A.toAlgCat ≃ₐ[K] Matrix (Fin n) (Fin n) K)

theorem trivialBrauer (K : Type u_1) [Field K] [Finite K] (a : BrauerGroup K) : a = 1

@[implicit_reducible]

noncomputable instance BrauerOverFinite (K : Type u_1) [Field K] [Finite K] : Unique (BrauerGroup K)

Equations

• BrauerOverFinite K = { default := 1, uniq := ⋯ }