mem_bot_iff_pow_eq_self — Mathlib

English

An element x lies in the prime subfield ⊥ if and only if x^p = x for characteristic p.

Русский

Элемент x лежит в простом подполе ⊥ тогда и только тогда, когда x^p = x при характеристике p.

LaTeX

$$$\\\\forall x \\\\in F, x \\\\in ⊥ \\\\Leftrightarrow x^{p} = x$$$

Lean4

theorem mem_bot_iff_pow_eq_self {x : F} : x ∈ (⊥ : Subfield F) ↔ x ^ p = x :=
  by
  have :=
    roots_X_pow_char_sub_X_bot F p ▸
      Polynomial.roots_map (Subfield.subtype _) (splits_bot F p) ▸ Multiset.mem_map (b := x)
  simpa [sub_eq_zero, iff_comm, FiniteField.X_pow_card_sub_X_ne_zero F (Fact.out : p.Prime).one_lt]

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