card' — Mathlib

English

There exists a prime p and an exponent n such that CharP K p and card K = p^n.

Русский

Существует простое p и показатель n, такие что CharP K p и card K = p^n.

LaTeX

$$$\exists p\text{ prime},\;\exists n \in \mathbb{N}_{>0},\; \text{CharP } K p \land |K| = p^{n}$$$

Lean4

theorem card' : ∃ (p : ℕ), CharP K p ∧ ∃ (n : ℕ+), Nat.Prime p ∧ Fintype.card K = p ^ (n : ℕ) :=
  let ⟨p, hc⟩ := CharP.exists K
  ⟨p, hc, @FiniteField.card K _ _ p hc⟩

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