birkhoffAverage_congr_ring — Mathlib

English

For two division semirings R and S with a module structure on M, birkhoffAverage_R equals birkhoffAverage_S for all f,g,n,x; i.e., the average does not depend on the ambient coefficient ring when comparing these two settings.

Русский

Для двух полускольных колец R и S с модулем M среднее Биркхоффа не зависит от выбранного кольца в рамках сопоставления birkhoffAverage: birkhoffAverage_R = birkhoffAverage_S.

LaTeX

$$$\forall R,S,\ birkhoffAverage(R,f,g,n,x) = birkhoffAverage(S,f,g,n,x).$$$

Lean4

theorem birkhoffAverage_congr_ring (S : Type*) [DivisionSemiring S] [Module S M] (f : α → α) (g : α → M) (n : ℕ)
    (x : α) : birkhoffAverage R f g n x = birkhoffAverage S f g n x :=
  map_birkhoffAverage R S (AddMonoidHom.id M) f g n x

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