coeff_iterate_frobenius — Mathlib

English

Let f ∈ Ring.Perfection R p and m,n ∈ ℕ. Then coeff R p (n+m) ((frobenius _ p)^[m] f) = coeff R p n f, i.e., iterating Frobenius shifts the index by m.

Русский

Пусть f ∈ Ring.Perfection R p и m,n ∈ ℕ. Тогда coeff R p (n+m) ((frobenius _ p)^[m] f) = coeff R p n f, т.е. повторная итерация Фробениуса сдвигает индекс на m.

LaTeX

$$$\\operatorname{coeff} R p (n+m) \\big((\\mathrm{frobenius}_{p})^{[m]} f\\big) = \\operatorname{coeff} R p n f$$$

Lean4

theorem coeff_iterate_frobenius (f : Ring.Perfection R p) (n m : ℕ) :
    coeff R p (n + m) ((frobenius _ p)^[m] f) = coeff R p n f :=
  Nat.recOn m rfl fun m ih => by rw [Function.iterate_succ_apply', Nat.add_succ, coeff_frobenius, ih]

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