coe_map

Mathlib.LinearAlgebra.Basis.Defs

URI: https://scilib.ai/kg/mathlib#Module.Basis.coe_map

English

The underlying function of the mapped basis is the composition of the original basis' function with f.

Русский

Основная функция отображения базиса после применения отображения равна композиции исходной функции базиса и f.

LaTeX

$$$(b.map f) = b \circ f$$$

Lean4

theorem coe_map : (b.map f : ι → M') = f ∘ b :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru