mapQ

Mathlib.RingTheory.Nilpotent.Lemmas

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

English

If f is nilpotent, the induced map on a submodule Q has the same nilpotency exponent.

Русский

Если $f$ нильпотентен, соответствующее отображение на quotient сохраняет ту же степень нильпотентности.

LaTeX

$$IsNilpotent (p.mapQ p f hp)$$

Lean4

theorem mapQ (hnp : IsNilpotent f) : IsNilpotent (p.mapQ p f hp) :=
  by
  obtain ⟨k, hk⟩ := hnp
  use k
  simp [← p.mapQ_pow, hk]

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

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

Разделы

Аффилиация

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