card_bot — Mathlib

English

The prime subfield ⊥ has exactly p elements, where p is the characteristic prime of F.

Русский

Простое подполе ⊥ имеет ровно p элементов, где p — простая характеристика поля.

LaTeX

$$$\\\\forall F \\\\text{field}, \\\\text{char}(F)=p \\\\Rightarrow \\\\#⊥=p$$$

Lean4

theorem card_bot : Nat.card (⊥ : Subfield F) = p := by
  rw [← fieldRange_castHom_eq_bot p, ← Nat.card_eq_of_bijective _ (RingHom.rangeRestrictField_bijective _),
    Nat.card_zmod]

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