coeff_map — Mathlib

English

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

Русский

Для f в Ring.Perfection R p и любых m,n ∈ ℕ соответствует: coeff R p (n+m) ((frobenius_p)^[m] f) = coeff R p n f.

LaTeX

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

Lean4

theorem coeff_map (φ : R →+* S) (f : Ring.Perfection R p) (n : ℕ) : coeff S p n (map p φ f) = φ (coeff R p n f) :=
  rfl

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