coeff_single_same — Mathlib

English

In a Hahn series that has a single nonzero coefficient at a, the coefficient at a is r.

Русский

В ряде Ханна, у которого единственный ненулевой коэффициент расположен в позиции a, коэффициент при a равен r.

LaTeX

$$$(\text{single } a\; r).\mathrm{coeff}(a) = r$$$

Lean4

@[simp]
theorem coeff_single_same (a : Γ) (r : R) : (single a r).coeff a = r := by
  classical exact Pi.single_eq_same (M := fun _ => R) a r

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