toFinsupp_algebraMap — Mathlib

English

For any r ∈ R, the toFinsupp of algebraMap R A[X] r equals the canonical algebraMap from R to AddMonoidAlgebra A ℕ applied to r.

Русский

Для каждого r ∈ R toFinsupp(algebraMap R A[X] r) равен каноническому algebraMap из R в AddMonoidAlgebra A ℕ applied к r.

LaTeX

$$$ (algebraMap R A[X] r).toFinsupp = \mathsf{algebraMap}_R^{\mathrm{AddMonoidAlgebra}\; A\; \mathbb{N}}\; r $$$

Lean4

@[simp]
theorem toFinsupp_algebraMap (r : R) : (algebraMap R A[X] r).toFinsupp = algebraMap R _ r :=
  show toFinsupp (C (algebraMap _ _ r)) = _ by
    rw [toFinsupp_C]
    rfl

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