coeff_toSubring — Mathlib

English

The coefficient of the lifted subring polynomial equals the original coefficient, after identifying it with the subring.

Русский

Коэффициент подкольцевого полинома равен исходному коэффициенту после соответствующего преобразования.

LaTeX

$$$\\uparrow\\mathrm{coeff}((\\mathrm{toSubring}\\ p\\ T\\ hp)\\,n) = \\mathrm{coeff}\\ p\\ n$$$

Lean4

@[simp]
theorem coeff_toSubring {n : ℕ} : ↑(coeff (toSubring p T hp) n) = coeff p n := by
  classical
  simp only [toSubring, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq', Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl

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