join₁_rename — Mathlib

English

The join₁ of a rename equals bind₁: join₁ (rename f φ) = bind₁ f φ.

Русский

Объединение join₁ после переименования равно связыванию bind₁: join₁ (rename f φ) = bind₁ f φ.

LaTeX

$$$\text{join}_1 (\text{rename } f \; \phi) = \text{bind}_1 f \; \phi$$$

Lean4

@[simp]
theorem join₁_rename (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) : join₁ (rename f φ) = bind₁ f φ :=
  aeval_id_rename _ _

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