π_relation

Mathlib.Algebra.Module.Presentation.Basic

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

English

For every relation r, π evaluated at the relation element is zero.

Русский

Для каждого отношения $r$ имеем $\pi(\text{relation}(r))=0$.

LaTeX

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

Lean4

@[simp]
theorem π_relation (r : relations.R) : solution.π (relations.relation r) = 0 :=
  solution.linearCombination_var_relation r

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

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

Разделы

Аффилиация

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