pow_map_zero_of_le

Mathlib.Algebra.Module.LinearMap.End

URI: https://scilib.ai/kg/mathlib#Module.End.pow_map_zero_of_le

← MathLib Explorer

English

If k ≤ l and (f^k)(m) = 0, then (f^l)(m) = 0 for any m in M.

Русский

Если k ≤ l и (f^k)(m) = 0, тогда для любого m ∈ M имеет место (f^l)(m) = 0.

LaTeX

$$$k \\le l \\Rightarrow (f^k)(m)=0 \\Rightarrow (f^l)(m)=0$ for all m.$$

Lean4

theorem pow_map_zero_of_le {f : End R M} {m : M} {k l : ℕ} (hk : k ≤ l) (hm : (f ^ k) m = 0) : (f ^ l) m = 0 := by
  rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]

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

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

Разделы

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

Аффилиация

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