ACounit — Mathlib

English

ACounit A B is the natural surjective algebra homomorphism MvPolynomial B A →ₐ[A] B given by X a ↦ a.

Русский

ACounit A B — естественный сюръективный алгебраический гомоморфизм MvPolynomial B A →ₐ[A] B, задающий X a ↦ a.

LaTeX

$$ACounit : MvPolynomial B A →ₐ[A] B := aeval id$$

Lean4

/-- `MvPolynomial.ACounit A B` is the natural surjective algebra homomorphism
`MvPolynomial B A →ₐ[A] B` obtained by `X a ↦ a`.

See `MvPolynomial.counit` for the “absolute” variant with `A = ℤ`,
and `MvPolynomial.counitNat` for the “absolute” variant with `A = ℕ`. -/
noncomputable def ACounit : MvPolynomial B A →ₐ[A] B :=
  aeval id

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