basisAux_tmul — Mathlib

English

For a basis b of M over R and A-algebra, the representation of a ∈ A under basis isomorphism matches tensor product with a.

Русский

Для базиса b модуля M над R и A-алгебры представление a в рамках изоморфизма базиса согласуется с тензорным произведением.

LaTeX

$$$(basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ b.repr.symm (Finsupp.single i 1)$$$

Lean4

theorem basisAux_tmul (a : A) (m : M) :
    basisAux A b (a ⊗ₜ m) = a • Finsupp.mapRange (algebraMap R A) (map_zero _) (b.repr m) :=
  by
  ext
  simp [basisAux, ← Algebra.commutes, Algebra.smul_def]

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