English
There exists a natural surjective ring homomorphism counit from MvPolynomial R ℤ to R, obtained by sending the indeterminate X_r to r.
Русский
Существует естественное сюръективное кольцевидное отображение counit: MvPolynomial R ℤ → R, такое что X_r ↦ r.
LaTeX
$$$\mathrm{counit}_R: \mathrm{MvPolynomial}(R, \mathbb{Z}) \to R\quad\text{with } X_r \mapsto r$$$
Lean4
/-- `MvPolynomial.counit R` is the natural surjective ring homomorphism
`MvPolynomial R ℤ →+* R` obtained by `X r ↦ r`.
See `MvPolynomial.ACounit` for a “relative” variant for algebras over a base ring,
and `MvPolynomial.counitNat` for the “absolute” variant with `R = ℕ`. -/
noncomputable def counit : MvPolynomial R ℤ →+* R :=
(ACounit ℤ R).toRingHom
