homQuotientZPowOfHom_comp — Mathlib

English

The composition of two quotient-power maps equals the quotient-power map of the composition.

Русский

Состав отображений по степеням факторного типа равен факторному отображению композиции.

LaTeX

$$homQuotientZPowOfHom (f.comp g) n = (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n)$$

Lean4

@[to_additive (attr := simp)]
theorem homQuotientZPowOfHom_comp :
    homQuotientZPowOfHom (f.comp g) n = (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n) :=
  monoidHom_ext _ rfl

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