algebraMapCoeffs_repr — Mathlib

English

The representation of the algebra-mapped basis is obtained by applying the map to the original representation coefficient-wise.

Русский

Показ представления базы после отображения по алгебраMap выполняется поэлементно через образ коэффициентов.

LaTeX

$$$$ (b.algebraMapCoeffs A h).repr m = (b.repr m).mapRange (algebraMap R A) (map_zero _) $$$$

Lean4

@[simp]
theorem algebraMapCoeffs_repr (m : M) :
    (b.algebraMapCoeffs A h).repr m = (b.repr m).mapRange (algebraMap R A) (map_zero _) := by rfl

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