pow_card_sub_one — Mathlib

English

In the finite field F_p with p prime, for any a ∈ F_p^×, a^{p-1} = 1; more generally, a^{p-1} = 1 if a ≠ 0 and 0 if a = 0.

Русский

В конечном поле F_p при простом p для любого a ∈ F_p^× верно a^{p-1} = 1; а в общем виде a^{p-1} = 1, если a ≠ 0, и 0, если a = 0.

LaTeX

$$$a^{p-1} = \begin{cases}1, & a \neq 0 \\ 0, & a = 0\end{cases}$$$

Lean4

theorem pow_card_sub_one (a : ZMod p) : a ^ (p - 1) = if a ≠ 0 then 1 else 0 :=
  by
  split_ifs with ha
  · exact pow_card_sub_one_eq_one ha
  · simp [of_not_not ha, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]

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