English
CentroidHom α injects into AddMonoidEnd α via its underlying function; i.e., the coercion to AddMonoidHom is injective.
Русский
CentroidHom α инъективно отображается в AddMonoidEnd α через свою базовую функцию; она инъективна.
LaTeX
$$Injective ((↑) : CentroidHom α → α →+ α)$$
Lean4
instance hasNPowNat : Pow (CentroidHom α) ℕ :=
⟨fun f n ↦
{ toAddMonoidHom := (f.toEnd ^ n : AddMonoid.End α)
map_mul_left' := fun a b ↦ by
induction n with
| zero => rfl
| succ n ih =>
rw [pow_succ']
exact (congr_arg f.toEnd ih).trans (f.map_mul_left' _ _)
map_mul_right' := fun a b ↦ by
induction n with
| zero => rfl
| succ n ih =>
rw [pow_succ']
exact (congr_arg f.toEnd ih).trans (f.map_mul_right' _ _) }⟩
