toMvPolynomial_id — Mathlib

English

For the identity linear map id on M1, id.toMvPolynomial b1 b1 equals X (the basic mv-polynomial).

Русский

Для тождественного отображения id на M1, id.toMvPolynomial b1 b1 равняется X (базовый mv-полином).

LaTeX

$$ (id : M1 →ₗ[R] M1).toMvPolynomial b1 b1 = X $$

Lean4

@[simp]
theorem toMvPolynomial_id : (id : M₁ →ₗ[R] M₁).toMvPolynomial b₁ b₁ = X := by unfold toMvPolynomial;
  simp only [toMatrix_id, Matrix.toMvPolynomial_one]

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