toMvPolynomial_one — Mathlib

English

The mv-polynomial associated to the identity matrix is the polynomial X (the sum of the variables in the standard notation).

Русский

mv-полином, соответствующий единичной матрице, равен полиному X (в классическом обозначении).

LaTeX

$$(1 : Matrix n n R).toMvPolynomial = X$$

Lean4

@[simp]
theorem toMvPolynomial_one [DecidableEq n] : (1 : Matrix n n R).toMvPolynomial = X :=
  by
  ext i : 1
  rw [toMvPolynomial, Finset.sum_eq_single i]
  · simp only [one_apply_eq, ← C_mul_X_eq_monomial, C_1, one_mul]
  · rintro j - hj
    simp only [one_apply_ne hj.symm, map_zero]
  · grind

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