coeff_frobenius — Mathlib

English

For any f in Ring.Perfection R p and n ∈ ℕ, the coefficient after applying Frobenius satisfies coeff R p (n+1) (frobenius _ p f) = coeff R p n f.

Русский

Для любого f в Ring.Perfection R p и натурального n выполняется coeff R p (n+1) (frobenius_p f) = coeff R p n f.

LaTeX

$$$\\operatorname{coeff} R p (n+1) (\\mathrm{frobenius}_{p} f) = \\operatorname{coeff} R p n f$$$

Lean4

theorem coeff_frobenius (f : Ring.Perfection R p) (n : ℕ) : coeff R p (n + 1) (frobenius _ p f) = coeff R p n f := by
  apply coeff_pow_p f n

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