support_pow'

Mathlib.Algebra.GroupWithZero.Indicator

URI: https://scilib.ai/kg/mathlib#Function.support_pow'

English

In the same setting as above, the support of f(a)^n equals the support of f(a); i.e., supp(f^n) = supp(f) when n ≠ 0.

Русский

В той же постановке опора f^n равна опоре f при n ≠ 0.

LaTeX

$$$ \operatorname{support}(f^n) = \operatorname{support}(f). $$$

Lean4

@[simp]
theorem support_pow' (f : ι → M₀) (hn : n ≠ 0) : support (f ^ n) = support f :=
  support_pow _ hn

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

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

Разделы

Аффилиация

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