coe_pow — Mathlib

English

The map sending an AlgHom to its linear map is a MonoidHom from AlgHom(R,A,A) to Module.End(R,A).

Русский

Отображение, отправляющее AlgHom к его линейному отображению, образует моноидоморфизм из AlgHom(R,A,A) в Module.End(R,A).

LaTeX

$$$$ \text{toEnd}: \mathrm{AlgHom}(R,A,A) \to^* \mathrm{Module.End}(R,A). $$$$

Lean4

@[simp]
theorem coe_pow (φ : A →ₐ[R] A) (n : ℕ) : ⇑(φ ^ n) = φ^[n] :=
  n.rec (by ext; simp) fun _ ih ↦ by ext; simp [pow_succ, ih]

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