not_isField_of_card_not_prime_pow

English

If a finite-type ring α has cardinality not a prime power, then α cannot be a field.

Русский

Если кардинал конечнопроизводного кольца не является степенью простого, то это кольцо не поле.

LaTeX

$$$\\neg\\mathrm{IsPrimePow}(|\\alpha|) \\Rightarrow \\neg \\mathrm{IsField}(\\alpha)$$$

Lean4

theorem not_isField_of_card_not_prime_pow {α} [Fintype α] [Ring α] : ¬IsPrimePow ‖α‖ → ¬IsField α :=
  mt fun h => Fintype.nonempty_field_iff.mp ⟨h.toField⟩

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