iterateFrobenius_zero_apply — Mathlib

English

Let R be a commutative semiring and p a natural with ExpChar R p. Then for every x in R, the zero-th iterate of Frobenius fixes x: (iterateFrobenius R p 0)(x) = x.

Русский

Пусть R — коммутативное полугруппа, p — натуральное число и ExpChar R p. Тогда для каждого x ∈ R выполняется: (iterateFrobenius R p 0)(x) = x.

LaTeX

$$$\forall x \in R,\ (\operatorname{iterateFrobenius} R p 0)(x) = x$$$

Lean4

theorem iterateFrobenius_zero_apply : iterateFrobenius R p 0 x = x := by rw [iterateFrobenius_def, pow_zero, pow_one]

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