postcomp_desc

Mathlib.Algebra.Module.Presentation.Basic

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

English

The composition of the desc map with the presentation π-map equals the given π-map of the solution.

Русский

Составление отображения desc с отображением π презентации равно π-отображению решения.

LaTeX

$$$$ (h.desc\\, s) \\circ solution.\\pi = s.\\pi $$$$

Lean4

@[simp]
theorem postcomp_desc (s : relations.Solution N) : solution.postcomp (h.desc s) = s := by aesop

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

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

Разделы

Аффилиация

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