π_comp_map_apply

Mathlib.Algebra.Module.Presentation.Basic

URI: https://scilib.ai/kg/mathlib#Module.Relations.Solution.π_comp_map_apply

← MathLib Explorer

English

For every x, π applied to map x equals zero.

Русский

Для каждого $x$ имеется $π(map(x))=0$.

LaTeX

$$$\forall x,\; \text{solution.π}(\text{relations.map}(x)) = 0$$$

Lean4

@[simp]
theorem π_comp_map_apply (x : relations.R →₀ A) : solution.π (relations.map x) = 0 :=
  by
  change solution.π.comp relations.map x = 0
  rw [π_comp_map, LinearMap.zero_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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