congr_zero

Mathlib.Analysis.Calculus.FormalMultilinearSeries

URI: https://scilib.ai/kg/mathlib#FormalMultilinearSeries.congr_zero

English

If k = l and p k = 0, then p l = 0 for a formal multilinear series p.

Русский

Если k = l и p k = 0, то p l = 0 для формальной многочленыой серии p.

LaTeX

$$Eq k l → Eq (p k) 0 → Eq (p l) 0$$

Lean4

theorem congr_zero (p : FormalMultilinearSeries 𝕜 E F) {k l : ℕ} (h : k = l) (h' : p k = 0) : p l = 0 := by subst h;
  exact h'

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

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

Разделы

Аффилиация

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