join₂_map — Mathlib

English

There is a natural equality involving join₂ and eval₂Hom with identity on R.

Русский

Существует естественная эквивалентность между join₂ и eval₂Hom с единицей на R.

LaTeX

$$Eq MvPolynomial.join₂ (MvPolynomial.eval₂Hom (RingHom.id (MvPolynomial σ R)) MvPolynomial.X)$$

Lean4

@[simp]
theorem join₂_map (f : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R) : join₂ (map f φ) = bind₂ f φ := by
  simp only [join₂, bind₂, eval₂Hom_map_hom, RingHom.id_comp]

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