desc_comp_π

Mathlib.Algebra.Module.Presentation.Basic

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

English

Desc is compatible with equality of solutions; if two solutions are equal, their generated desc maps agree.

Русский

Desc совместим с равенством решений; если два решения равны, их отображения desc совпадают.

LaTeX

$$$$ s = s' \\implies h.desc\\, s = h.desc\\, s' $$$$

Lean4

@[simp]
theorem desc_comp_π (s : relations.Solution N) : (h.desc s).comp solution.π = s.π := by aesop

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

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

Разделы

Аффилиация

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