toGenerators_comp — Mathlib

English

The toGenerators of the composed presentation equals the composition of toGenerators: (Q.comp P).toGenerators = Q.toGenerators.comp P.toGenerators.

Русский

Генераторы склеенной презентации равны композиции генераторов: (Q.comp P).toGenerators = Q.toGenerators.comp P.toGenerators.

LaTeX

$$$\\mathrm{toGenerators\\_comp}:\\; (Q.comp P).toGenerators = Q.toGenerators.comp P.toGenerators$$$

Lean4

theorem toGenerators_comp : (Q.comp P).toGenerators = Q.toGenerators.comp P.toGenerators :=
  rfl

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