matrixEquivTensor_apply_single — Mathlib

English

The symmetric application of matrixEquivTensor maps a ⊗ M to a · M mapped by algebra map.

Русский

Симметричное применение matrixEquivTensor переводит a ⊗ M в a · M, отображенную алгебраической картой.

LaTeX

$$$ (matrixEquivTensor\,n\,R\,A).symm (a \otimes_\mathrm{T} M) = a \cdot M.map(\mathrm{algebraMap}_{R}^{A}) $$$

Lean4

@[simp high]
theorem matrixEquivTensor_apply_single (i j : n) (x : A) : matrixEquivTensor n R A (single i j x) = x ⊗ₜ single i j 1 :=
  by
  have t : ∀ p : n × n, i = p.1 ∧ j = p.2 ↔ p = (i, j) := by aesop
  simp [ite_tmul, t, single]

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