MvPolynomial.ACounit_X

theorem MvPolynomial.ACounit_X : ∀ (A : Type u_1) {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B] (b : B), (MvPolynomial.ACounit A B) (MvPolynomial.X b) = b

The theorem `MvPolynomial.ACounit_X` states that for all types `A` and `B`, where `A` is a commutative semiring and `B` is a commutative semiring that is also an `A`-algebra, and for any element `b` of `B`, when the algebra homomorphism `MvPolynomial.ACounit A B` is applied to the degree `1` monomial `MvPolynomial.X b`, the result is `b`. Intuitively, this means that `MvPolynomial.ACounit A B` maps the monomial `X_b` to the element `b` in `B`.

More concisely: For any commutative semirings `A` and `B` with `B` an `A`-algebra, the algebra homomorphism `MvPolynomial.ACounit A B` maps the degree `1` monomial `MvPolynomial.X b` to the element `b` in `B`.