basis_repr_tmul — Mathlib

English

The basis for A ⊗R M is defined by a basisAux isomorphism, giving a canonical A-basis from an R-basis of M.

Русский

Базис для A ⊗R M задаётся через базисный изоморфизм basisAux, формирующий канонический A-базис из R-базиса M.

LaTeX

$$$basis A b$$$

Lean4

@[simp]
theorem basis_repr_tmul (a : A) (m : M) :
    (basis A b).repr (a ⊗ₜ m) = a • Finsupp.mapRange (algebraMap R A) (map_zero _) (b.repr m) :=
  basisAux_tmul b _ _

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