English
join₂ is the monadic join corresponding to bind₂, obtained by evaluating the inner polynomials with the identity on coefficients.
Русский
join₂ является монадной операцией объединения, соответствующей bind₂, полученной путем вычисления внутренних полиномов по идентичности коэффициентов.
LaTeX
$$$\text{join}_2 : \operatornameMvPolynomial(σ, \operatornameMvPolynomial(σ,R)) \to \operatornameMvPolynomial(σ,R)$$$
Lean4
/-- `join₂` is the monadic join operation corresponding to `MvPolynomial.bind₂`. Given a polynomial `p`
with variables in `σ` whose coefficients are polynomials in `σ` with coefficients in `R`,
`join₂ p` collapses `p` to a polynomial with variables in `σ` and coefficients in `R`.
This operation is a ring hom.
-/
def join₂ : MvPolynomial σ (MvPolynomial σ R) →+* MvPolynomial σ R :=
eval₂Hom (RingHom.id _) X
