birkhoffAverage_congr_ring' — Mathlib

English

A variant stating birkhoffAverage with respect to R equals birkhoffAverage with respect to S for all f,g when mapping through the identity on M; i.e., birkhoffAverage (α := α) (M := M) R = birkhoffAverage S.

Русский

Вариант утверждает, что birkhoffAverage одинаково определяется независимо от кольца R или S через единичное отображение на M: birkhoffAverage_R = birkhoffAverage_S.

LaTeX

$$$\mathrm{birkhoffAverage}(R) = \mathrm{birkhoffAverage}(S).$$$

Lean4

theorem birkhoffAverage_congr_ring' (S : Type*) [DivisionSemiring S] [Module S M] :
    birkhoffAverage (α := α) (M := M) R = birkhoffAverage S := by ext; apply birkhoffAverage_congr_ring

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