map_expand — Mathlib

English

The general coefficient formula for expansion states that for p > 0,

Русский

Общая формула коэффициентов после расширения: для p > 0,

LaTeX

$$$(\operatorname{expand}(R,p) f).\mathrm{coeff}_n = \begin{cases} f.\mathrm{coeff}(n/p), & p \mid n, \\ 0, & \text{otherwise} \end{cases}$$$

Lean4

theorem map_expand {p : ℕ} {f : R →+* S} {q : R[X]} : map f (expand R p q) = expand S p (map f q) :=
  by
  by_cases hp : p = 0
  · simp [hp]
  ext
  rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]
  split_ifs <;> simp_all

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