coeff_iterate_frobenius' — Mathlib

English

For f ∈ Ring.Perfection R p and n,m ∈ ℕ with m ≤ n, coeff R p n ((frobenius _ p)^[m] f) = coeff R p (n-m) f.

Русский

Для f ∈ Ring.Perfection R p и n,m ∈ ℕ с условием m ≤ n выполняется coeff R p n ((frobenius _ p)^[m] f) = coeff R p (n-m) f.

LaTeX

$$$\\operatorname{coeff} R p n\\big((\\mathrm{frobenius}_{p})^{[m]} f\\big) = \\operatorname{coeff} R p (n-m) f$ при m \\le n$$

Lean4

theorem coeff_iterate_frobenius' (f : Ring.Perfection R p) (n m : ℕ) (hmn : m ≤ n) :
    coeff R p n ((frobenius _ p)^[m] f) = coeff R p (n - m) f :=
  Eq.symm <| (coeff_iterate_frobenius _ _ m).symm.trans <| (tsub_add_cancel_of_le hmn).symm ▸ rfl

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