map_expand_pow_char — Mathlib

English

If n ∈ ℕ, then map (frobenius R p)^n (expand R (p^n) f) = f^{p^n}.

Русский

Если n ∈ ℕ, то map (frobenius_R(p))^n (expand_R(p^n, f)) = f^{p^n}.

LaTeX

$$$$\mathrm{map}(\mathrm{frobenius}_R(p)^{n})\bigl(\mathrm{expand}_R(p^{n},f)\bigr)=f^{p^{n}}$$$$

Lean4

theorem map_expand_pow_char (f : R[X]) (n : ℕ) : map (frobenius R p ^ n) (expand R (p ^ n) f) = f ^ p ^ n := by
  induction n with
  | zero => simp [RingHom.one_def]
  | succ _ n_ih =>
    symm
    rw [pow_succ, pow_mul, ← n_ih, ← expand_char, pow_succ', RingHom.mul_def, ← map_map, mul_comm, expand_mul, ←
      map_expand]

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