fromQuotient_toQuotient

Mathlib.Algebra.Module.Presentation.Basic

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

English

The composition fromQuotient after toQuotient equals π.

Русский

Сложение fromQuotient после toQuotient даёт π.

LaTeX

$$$\text{solution.fromQuotient} \circ \text{relations.toQuotient} = \text{solution.π}$$$

Lean4

@[simp]
theorem fromQuotient_toQuotient (x : relations.G →₀ A) :
    solution.fromQuotient (relations.toQuotient x) = solution.π x :=
  rfl

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

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

Разделы

Аффилиация

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