frobenius_neg — Mathlib

English

Let R be a commutative ring and p ∈ ℕ with ExpChar R p. Then the Frobenius endomorphism φ_R,p satisfies φ_R,p(−x) = −φ_R,p(x) for all x ∈ R.

Русский

Пусть R — коммутативное кольцо и p ∈ ℕ так, что R имеет ExpChar R p. Тогда отображение Фробениуса φ_R,p удовлетворяет φ_R,p(−x) = −φ_R,p(x) для всех x ∈ R.

LaTeX

$$$\operatorname{frobenius}(R,p)(-x) = -\operatorname{frobenius}(R,p)(x)$$$

Lean4

theorem frobenius_neg : frobenius R p (-x) = -frobenius R p x :=
  map_neg ..

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