coeff_comp_monomial — Mathlib

English

For every n, the composition of the coefficient map with the monomial map is the identity on R.

Русский

Для каждого n композиция коэффициентной карты с мономиальной картой равна тождению на R.

LaTeX

$$$$ (\operatorname{coeff}_n) \circ (\operatorname{monomial}_n) = \mathrm{id}_R $$$$

Lean4

@[simp]
theorem coeff_comp_monomial (n : ℕ) : (coeff (R := R) n).comp (monomial n) = LinearMap.id :=
  LinearMap.ext <| coeff_monomial_same n

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