toMvPolynomial_comp — Mathlib

English

For g: M2 → M3 and f: M1 → M2, the mv-polynomial of the composed map g ∘ f satisfies (g ∘ f).toMvPolynomial i = bind₁ (f.toMvPolynomial b1 b2) (g.toMvPolynomial b2 b3 i).

Русский

Для композиции mv-полиномов выполняется (g ∘ f).toMvPolynomial i = bind₁ (f.toMvPolynomial b1 b2) (g.toMvPolynomial b2 b3 i).

LaTeX

$$$ (g \\circ f).toMvPolynomial b_1 b_3 i = \\bind_1 (f.toMvPolynomial b_1 b_2) (g.toMvPolynomial b_2 b_3 i) $$$

Lean4

theorem toMvPolynomial_comp (g : M₂ →ₗ[R] M₃) (f : M₁ →ₗ[R] M₂) (i : ι₃) :
    (g ∘ₗ f).toMvPolynomial b₁ b₃ i = bind₁ (f.toMvPolynomial b₁ b₂) (g.toMvPolynomial b₂ b₃ i) :=
  by
  simp only [toMvPolynomial, toMatrix_comp b₁ b₂ b₃, Matrix.toMvPolynomial_mul]
  rfl

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