coeff — Mathlib

English

For each x ∈ X, the coefficient map coeff(x) is a group homomorphism from FreeAbelianGroup X to ℤ, extracting the multiplicity of x in a formal sum.

Русский

Для каждого x ∈ X отображение coeff(x) является гомоморфизмом группы FreeAbelianGroup X в ℤ и извлекает кратность появления x в формальной сумме.

LaTeX

$$$FreeAbelianGroup.coeff(x) : FreeAbelianGroup X \\to_{+} \\mathbb{Z}$ with coeff(x) = (Finsupp.applyAddHom x) \\circ toFinsupp$$

Lean4

/-- `coeff x` is the additive group homomorphism `FreeAbelianGroup X →+ ℤ`
that sends `a` to the multiplicity of `x : X` in `a`. -/
def coeff (x : X) : FreeAbelianGroup X →+ ℤ :=
  (Finsupp.applyAddHom x).comp toFinsupp

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