homQuotientZPowOfHom_id — Mathlib

English

The identity homomorphism induces the identity map on the corresponding quotients by Z-powers.

Русский

Тождественный гомоморфизм индуцирует тождественный отображение на соответствующих фактор-группах по Z-степеням.

LaTeX

$$homQuotientZPowOfHom_id : homQuotientZPowOfHom (MonoidHom.id A) n = MonoidHom.id _$$

Lean4

@[to_additive (attr := simp)]
theorem homQuotientZPowOfHom_id : homQuotientZPowOfHom (MonoidHom.id A) n = MonoidHom.id _ :=
  monoidHom_ext _ rfl

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