counitNat — Mathlib

English

There is a natural surjective ring homomorphism counitNat from MvPolynomial A ℕ to A, given by X_a ↦ a.

Русский

Существует естественное сюръективное кольцевое отображение counitNat: MvPolynomial A ℕ → A, такое что X_a ↦ a.

LaTeX

$$$\mathrm{counitNat}_A: \mathrm{MvPolynomial}(A, \mathbb{N}) \to A\quad\text{with } X_a \mapsto a$$$

Lean4

/-- `MvPolynomial.counitNat A` is the natural surjective ring homomorphism
`MvPolynomial A ℕ →+* A` obtained by `X a ↦ a`.

See `MvPolynomial.ACounit` for a “relative” variant for algebras over a base ring
and `MvPolynomial.counit` for the “absolute” variant with `A = ℤ`. -/
noncomputable def counitNat : MvPolynomial A ℕ →+* A :=
  ACounit ℕ A

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