English
A basic building block: matPolyEquiv maps a single-entry polynomial matrix to a monomial in the corresponding single-entry polynomial matrix.
Русский
Базовый элемент: matPolyEquiv переводит матрицу с единичной полиномой в моном по соответствующей позиции.
LaTeX
$$$\\text{matPolyEquiv}(\\text{single } i j \\lvert\\!\\text{monomial } k x) = \\text{monomial } k \\big( \\text{single } i j x \\big)$$$
Lean4
theorem matPolyEquiv_coeff_apply_aux_1 (i j : n) (k : ℕ) (x : R) :
matPolyEquiv (single i j <| monomial k x) = monomial k (single i j x) :=
by
simp only [matPolyEquiv, AlgEquiv.trans_apply, matrixEquivTensor_apply_single]
apply (polyEquivTensor R (Matrix n n R)).injective
simp only [AlgEquiv.apply_symm_apply, Algebra.TensorProduct.comm_tmul, polyEquivTensor_apply, eval₂_monomial]
simp only [one_pow, Algebra.TensorProduct.tmul_pow]
rw [← smul_X_eq_monomial, ← TensorProduct.smul_tmul]
congr with i' <;> simp [single]
