birkhoffAverage_zero — Mathlib

English

For any f, g, and x, the Birkhoff average with n = 0 equals the zero element of M: birkhoffAverage_R f g 0 x = 0.

Русский

Для любых f, g и x среднее Биркхоффа при n = 0 равно нулю в целевом модуле: birkhoffAverage_R f g 0 x = 0.

LaTeX

$$$\mathrm{birkhoffAverage}(R,f,g,0,x) = 0.$$$

Lean4

theorem birkhoffAverage_zero (f : α → α) (g : α → M) (x : α) : birkhoffAverage R f g 0 x = 0 := by
  simp [birkhoffAverage]

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