map_comp_ι

Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#ExteriorAlgebra.map_comp_ι

English

The map induced by f commutes with the natural embedding ι: map f composed with ι equals ι composed with f.

Русский

Индукция отображения map f коммутирует с естественным вложением ι: map f ∘ ι = ι ∘ f.

LaTeX

$$$ (map f) \\circ ι_R = ι_R \\circ f. $$$

Lean4

@[simp]
theorem map_comp_ι (f : M →ₗ[R] N) : (map f).toLinearMap ∘ₗ ι R = ι R ∘ₗ f :=
  CliffordAlgebra.map_comp_ι _

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

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

Разделы

Аффилиация

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