card — Mathlib

English

If two finite fields have the same cardinality, then they are algebraically isomorphic (over ZMod p).

Русский

Если два конечных поля имеют одинаковую кардинальность, то они алгебраически изоморфны (относительно ZMod p).

LaTeX

$$algEquivOfCardEq (hKK' : Fintype.card K = Fintype.card K') : K ≃ₐ[ZMod p] K'$$

Lean4

theorem card (h : n ≠ 0) : Nat.card (GaloisField p n) = p ^ n :=
  by
  let b := IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
  haveI : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)
  rw [Nat.card_eq_fintype_card, Module.card_fintype b, ← Module.finrank_eq_card_basis b, ZMod.card, finrank p h]

Похожие утверждения