powersMulHom

Mathlib.Algebra.Group.Nat.Hom

URI: https://scilib.ai/kg/mathlib#powersMulHom

← MathLib Explorer

English

For all f : ℕ →+ M and n : Nat, (multiplesAddHom M) f n = n • f 1.

Русский

Для всех f : ℕ →+ M и n : Nat, (multiplesAddHom M) f n = n • f(1).

LaTeX

$$$ (multiplesAddHom M) f n = n \cdot f(1) $$$

Lean4

/-- If `M` is commutative, `powersHom` is a multiplicative equivalence. -/
def powersMulHom : M ≃* (Multiplicative ℕ →* M) where
  __ := powersHom M
  map_mul' a b := MonoidHom.ext fun n ↦ by simp [mul_pow]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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