iterateFrobenius_add_apply — Mathlib

English

For all m,n ∈ ℕ and x ∈ R, Frobenius iterates satisfy additivity in the exponent: (iterateFrobenius R p (m+n)) x = (iterateFrobenius R p m)((iterateFrobenius R p n) x).

Русский

Для любых m,n ∈ ℕ и x ∈ R выполняется аддитивность по степеням итерирования Фробениуса: (iterateFrobenius R p (m+n)) x = (iterateFrobenius R p m)((iterateFrobenius R p n) x).

LaTeX

$$$\forall x \in R,\ (\iterateFrobenius R p (m+n))\,x = (\iterateFrobenius R p m)\bigl((\iterateFrobenius R p n)\,x\bigr)$$$

Lean4

theorem iterateFrobenius_add_apply :
    iterateFrobenius R p (m + n) x = iterateFrobenius R p m (iterateFrobenius R p n x) := by
  simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]

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