mul_apply

Mathlib.Algebra.Module.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#LinearEquiv.mul_apply

English

For e ∈ Aut_R(M) and n ∈ ℕ, (e^n)(m) = e^[n](m) for all m ∈ M.

Русский

Для e ∈ Aut_R(M) и n ∈ ℕ верно (e^n)(m) = e^[n](m) для всех m ∈ M.

LaTeX

$$$ (e^n) m = e^{[n]} m $$$

Lean4

@[simp]
theorem mul_apply (f : M ≃ₗ[R] M) (g : M ≃ₗ[R] M) (x : M) : (f * g) x = f (g x) :=
  rfl

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

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

Разделы

Аффилиация

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